Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 18 2022 at 10:01):

From: clefort <ipub@charter.net>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 10:01):

From: Peter Lammich <peter.lammich@uni-muenster.de>
clefort wrote:

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

end

Greetings Peter

Last updated: May 03 2024 at 08:18 UTC