[isabelle] "Knaster_Tarski" Theorem? in Proof General
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?
Clinton R. LeFort
This archive was generated by a fusion of
Pipermail (Mailman edition) and