Re: [isabelle] How to fix it?

In your two examples you need to relace ~X by (~X).


Lucas Cavalcante schrieb:
I'd like to provetheorem negeq: "EX xs. ((neg_eq Formula) = ~xs (*here*) | (neq_eq Formula) = xs)"
Applying induction over Formula, but Isar says "Inner lexical error at: = ~xs". Just as happen at neg_eq's recursive funcion definition:
consts neg_eq :: "sbf => sbf"
primrec "neg_eq P = P" (*here*)
"neg_eq ~P = ~P"
"neg_eq ~~P = neg_eq P"
 Isar says "Inner lexical error at: = P".How to fix it?Regards,LucasPS.: THIS MENSAGE: (, THE THEORY: (
Veja só alguns dos novos serviços online no Windows Live Ideas — são tão novos que ainda não foram disponibilizados oficialmente.

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