[isabelle] "Knaster_Tarski" Theorem? in Proof General





Hello,

I'm trying to follow the steps of Dr. Wenzel's Thesis paper and explanations of Isabelle/Isar protocol, but when placing the Knaster_Tarski Theorem in Proof General window I get this result when doing Next step:

theory Knaster_Tarski :  "( /\x y x ... --> f a = a)"

In the Proof General window I have placed the actual theory which Dr. Wenzel gives in his thesis. When I do next Proof General does not 'highlight' in light blue the theory, but as said earlier, only gives the response below.

Response:  *** Outer syntax error: keyboard "imports" expected,
                    ***but kywordr ":" was found

I have Isabelle/Isar 2005. Would there be a problem in the way I stated the theory?

Thank you,

Clinton R. LeFort





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