[isabelle] How to fix it?



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: (http://paste.ubuntubrasil.org/4300), THE THEORY: (http://paste.ubuntubrasil.org/4299).
_________________________________________________________________
Veja só alguns dos novos serviços online no Windows Live Ideas — são tão novos que ainda não foram disponibilizados oficialmente.
http://ideas.live.com



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