Re: [isabelle] "Knaster_Tarski" Theorem? in Proof General



clefort wrote:



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)"


try:
theory Knaster_Tarski
imports Main
begin
 lemma "( /\x y x ... --> f a = a)" ...

end

Greetings Peter






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