reset HOL_quantifiers by default;
authorwenzelm
Mon Jun 07 21:22:18 1999 +0200 (1999-06-07)
changeset 679535f214e73668
parent 6794 ac367328b875
child 6796 c2e5cb8cd50d
reset HOL_quantifiers by default;
NEWS
src/HOL/HOL.thy
     1.1 --- a/NEWS	Mon Jun 07 19:25:12 1999 +0200
     1.2 +++ b/NEWS	Mon Jun 07 21:22:18 1999 +0200
     1.3 @@ -116,6 +116,9 @@
     1.4  * HOL/recdef (TFL): requires theory Recdef; 'congs' syntax now expects
     1.5  comma separated list of theorem names rather than an ML expression;
     1.6  
     1.7 +* reset HOL_quantifiers by default, i.e. quantifiers are printed as
     1.8 +ALL/EX rather than !/?;
     1.9 +
    1.10  
    1.11  *** ZF ***
    1.12  
     2.1 --- a/src/HOL/HOL.thy	Mon Jun 07 19:25:12 1999 +0200
     2.2 +++ b/src/HOL/HOL.thy	Mon Jun 07 21:22:18 1999 +0200
     2.3 @@ -212,7 +212,7 @@
     2.4  
     2.5  (** Choice between the HOL and Isabelle style of quantifiers **)
     2.6  
     2.7 -val HOL_quantifiers = ref true;
     2.8 +val HOL_quantifiers = ref false;
     2.9  
    2.10  fun alt_ast_tr' (name, alt_name) =
    2.11    let