adapted to qualified names;
authorwenzelm
Mon Oct 20 11:06:01 1997 +0200 (1997-10-20)
changeset 39421f1c1f524d19
parent 3941 ea440c63d206
child 3943 b6e0c90f3bf4
adapted to qualified names;
src/FOLP/IFOLP.thy
src/FOLP/ROOT.ML
     1.1 --- a/src/FOLP/IFOLP.thy	Mon Oct 20 11:01:07 1997 +0200
     1.2 +++ b/src/FOLP/IFOLP.thy	Mon Oct 20 11:06:01 1997 +0200
     1.3 @@ -8,6 +8,8 @@
     1.4  
     1.5  IFOLP = Pure +
     1.6  
     1.7 +global
     1.8 +
     1.9  classes term < logic
    1.10  
    1.11  default term
    1.12 @@ -59,6 +61,8 @@
    1.13   idpeel         :: "[p,'a=>p]=>p"
    1.14   nrm, NRM       :: "p"
    1.15  
    1.16 +local
    1.17 +
    1.18  rules
    1.19  
    1.20  (**** Propositional logic ****)
     2.1 --- a/src/FOLP/ROOT.ML	Mon Oct 20 11:01:07 1997 +0200
     2.2 +++ b/src/FOLP/ROOT.ML	Mon Oct 20 11:06:01 1997 +0200
     2.3 @@ -12,6 +12,8 @@
     2.4  
     2.5  writeln banner;
     2.6  
     2.7 +reset global_names;
     2.8 +
     2.9  print_depth 1;
    2.10  
    2.11  use_thy "IFOLP";