src/FOLP/IFOLP.thy
changeset 38522 de7984a7172b
parent 36452 d37c6eed8117
child 38800 34c84817e39c
     1.1 --- a/src/FOLP/IFOLP.thy	Wed Aug 18 12:19:27 2010 +0200
     1.2 +++ b/src/FOLP/IFOLP.thy	Wed Aug 18 12:26:48 2010 +0200
     1.3 @@ -12,8 +12,6 @@
     1.4  
     1.5  setup PureThy.old_appl_syntax_setup
     1.6  
     1.7 -global
     1.8 -
     1.9  classes "term"
    1.10  default_sort "term"
    1.11  
    1.12 @@ -63,8 +61,6 @@
    1.13   nrm            :: p
    1.14   NRM            :: p
    1.15  
    1.16 -local
    1.17 -
    1.18  syntax "_Proof" :: "[p,o]=>prop"    ("(_ /: _)" [51, 10] 5)
    1.19  
    1.20  ML {*