aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar/ex/Tarski.thy
diff options
context:
space:
mode:
Diffstat (limited to 'isar/ex/Tarski.thy')
-rw-r--r--isar/ex/Tarski.thy9
1 files changed, 4 insertions, 5 deletions
diff --git a/isar/ex/Tarski.thy b/isar/ex/Tarski.thy
index 9d4e8c0b..ec1247aa 100644
--- a/isar/ex/Tarski.thy
+++ b/isar/ex/Tarski.thy
@@ -1,17 +1,16 @@
(**********
- This file is copied from Isabelle2009-2.
- It has been beautified with Tokens \<rightarrow> Replace Shortcuts
+ This file is copied from Isabelle2011.
+ It has been beautified with Tokens -> Replace Shortcuts
**********)
(* Title: HOL/ex/Tarski.thy
- ID: $Id$
- Author: Florian Kammüller, Cambridge University Computer Laboratory
+ Author: Florian Kammüller, Cambridge University Computer Laboratory
*)
header {* The Full Theorem of Tarski *}
theory Tarski
-imports Main FuncSet
+imports Main "~~/src/HOL/Library/FuncSet"
begin
text {*