aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar/KnasterTarski.thy
diff options
context:
space:
mode:
Diffstat (limited to 'isar/KnasterTarski.thy')
-rw-r--r--isar/KnasterTarski.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/isar/KnasterTarski.thy b/isar/KnasterTarski.thy
index 2a1496e6..4e6961a8 100644
--- a/isar/KnasterTarski.thy
+++ b/isar/KnasterTarski.thy
@@ -9,7 +9,7 @@ Typical textbook proof example.
header {* Textbook-style reasoning: the Knaster-Tarski Theorem *}
-theory KnasterTarski = Main:
+theory KnasterTarski imports Main begin
subsection {* Prose version *}