removed HOL_quantifiers;
authorwenzelm
Tue Aug 17 22:14:08 1999 +0200 (1999-08-17)
changeset 7240a509730e424b
parent 7239 26685edee372
child 7241 8f3c14d60345
removed HOL_quantifiers;
src/HOL/AxClasses/Group/ROOT.ML
src/HOL/AxClasses/Lattice/ROOT.ML
src/HOL/AxClasses/Tutorial/ROOT.ML
src/HOL/UNITY/ROOT.ML
src/HOL/UNITY/UNITY.ML
     1.1 --- a/src/HOL/AxClasses/Group/ROOT.ML	Tue Aug 17 22:14:02 1999 +0200
     1.2 +++ b/src/HOL/AxClasses/Group/ROOT.ML	Tue Aug 17 22:14:08 1999 +0200
     1.3 @@ -5,7 +5,6 @@
     1.4  Some bits of group theory via axiomatic type classes.
     1.5  *)
     1.6  
     1.7 -reset HOL_quantifiers;
     1.8  set show_types;
     1.9  set show_sorts;
    1.10  
     2.1 --- a/src/HOL/AxClasses/Lattice/ROOT.ML	Tue Aug 17 22:14:02 1999 +0200
     2.2 +++ b/src/HOL/AxClasses/Lattice/ROOT.ML	Tue Aug 17 22:14:08 1999 +0200
     2.3 @@ -7,7 +7,6 @@
     2.4  
     2.5  open AxClass;
     2.6  
     2.7 -reset HOL_quantifiers;
     2.8  reset eta_contract;
     2.9  set show_types;
    2.10  set show_sorts;
     3.1 --- a/src/HOL/AxClasses/Tutorial/ROOT.ML	Tue Aug 17 22:14:02 1999 +0200
     3.2 +++ b/src/HOL/AxClasses/Tutorial/ROOT.ML	Tue Aug 17 22:14:08 1999 +0200
     3.3 @@ -7,7 +7,6 @@
     3.4  example resides in directory FOL/ex/.)
     3.5  *)
     3.6  
     3.7 -reset HOL_quantifiers;
     3.8  set show_types;
     3.9  set show_sorts;
    3.10  
     4.1 --- a/src/HOL/UNITY/ROOT.ML	Tue Aug 17 22:14:02 1999 +0200
     4.2 +++ b/src/HOL/UNITY/ROOT.ML	Tue Aug 17 22:14:08 1999 +0200
     4.3 @@ -9,7 +9,6 @@
     4.4  writeln"Root file for HOL/UNITY";
     4.5  
     4.6  set proof_timing;
     4.7 -set HOL_quantifiers;
     4.8  
     4.9  time_use_thy "UNITY";
    4.10  time_use_thy "Deadlock";
     5.1 --- a/src/HOL/UNITY/UNITY.ML	Tue Aug 17 22:14:02 1999 +0200
     5.2 +++ b/src/HOL/UNITY/UNITY.ML	Tue Aug 17 22:14:08 1999 +0200
     5.3 @@ -9,7 +9,6 @@
     5.4  *)
     5.5  
     5.6  set proof_timing;
     5.7 -HOL_quantifiers := false;
     5.8  
     5.9  
    5.10  (*** General lemmas ***)