[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:

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

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

Sincerely,
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.