[isabelle] Isar syntax question

I am learning Isar and have another naive question on the syntax:
I am trying to do something like this in Isar:

1: lemma
2:   shows "not something"
3: proof(rule ccontr)
4:  assume "something"
5:  thus False proof cases
6: 	...
7:   qed
8: qed

and get "*** Failed to refine any pending goal" error around line 5

Why this does not work? Something like this works instead:

  shows "not something"
 assume "something" 
 hence False proof cases
  thus False by simp

But last statement (thus False by simp) seems to be unnecessary, as it is proving
False from False!

Vadim Zaliva

CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.