src/FOL/IFOL.thy
changeset 38522 de7984a7172b
parent 36452 d37c6eed8117
child 39159 0dec18004e75
--- a/src/FOL/IFOL.thy	Wed Aug 18 12:19:27 2010 +0200
+++ b/src/FOL/IFOL.thy	Wed Aug 18 12:26:48 2010 +0200
@@ -28,8 +28,6 @@
 
 setup PureThy.old_appl_syntax_setup
 
-global
-
 classes "term"
 default_sort "term"
 
@@ -87,8 +85,6 @@
   Ex        (binder "\<exists>" 10) and
   Ex1       (binder "\<exists>!" 10)
 
-local
-
 finalconsts
   False All Ex
   "op ="