# [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.*