src/FOLP/IFOLP.thy
changeset 38522 de7984a7172b
parent 36452 d37c6eed8117
child 38800 34c84817e39c
--- a/src/FOLP/IFOLP.thy	Wed Aug 18 12:19:27 2010 +0200
+++ b/src/FOLP/IFOLP.thy	Wed Aug 18 12:26:48 2010 +0200
@@ -12,8 +12,6 @@
 
 setup PureThy.old_appl_syntax_setup
 
-global
-
 classes "term"
 default_sort "term"
 
@@ -63,8 +61,6 @@
  nrm            :: p
  NRM            :: p
 
-local
-
 syntax "_Proof" :: "[p,o]=>prop"    ("(_ /: _)" [51, 10] 5)
 
 ML {*