# Re: [isabelle] Isar syntax question

On Jul 16, 2014, at 15:12 , Lars Noschinski <noschinl at in.tum.de> wrote:
> Have a look ath the proof state after "proof (rule ccontr)". The
> precondition is "~~ something". Your assumption "something" does not
> unify with this, so you get an error message as soon as you try to
> discharge a proof obligation with show (or thus).
Thanks! That helps. The reason I used "something" instead of "~~something"
in the assumption is to be able to use simpler cases syntax as my "something"
is inductive definition:
inductive something :: .... where
C1: ... |
C2: ...
If I am proving "something" I can write "proof cases". If I proving ~~something
I have to write proof (cases something).
I do not know what is involved implementation-wiser but it would be nice if Isabelle could deal with
trivial double negation during unification.
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.*