[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:
2: shows "not something"
3: proof(rule ccontr)
4: assume "something"
5: thus False proof cases
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"
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!
CMU ECE PhD student
This archive was generated by a fusion of
Pipermail (Mailman edition) and