Re: [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)"
lemma "( /\x y x ... --> f a = a)" ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and