Isabelle Logic simple natural deduction test

Question

http://pastebin.com/1ZEt9r32

What is wrong with line 30? Isabelle says this "Failed to finish proof⌂: goal (2 subgoals): 1. ¬ P ⟹ Q 2. Q ⟹ ¬ P"

This is a theory for a natural deduction class

Answer 1

The order of the premises is in the wrong order. If you reorder them as follows, then the proof is accepted.

from pq and npq and qq show "Q" by (rule disjE)

You can inspect the expected order by

thm disjE

Hope this helps, René