# HG changeset patch
# User wenzelm
# Date 928783338 -7200
# Node ID 35f214e73668daf8cbf8be02e04e6ba8910a88a2
# Parent  ac367328b875df73e33868c0e8d1ee37c50c50a7
reset HOL_quantifiers by default;

diff -r ac367328b875 -r 35f214e73668 NEWS
--- a/NEWS	Mon Jun 07 19:25:12 1999 +0200
+++ b/NEWS	Mon Jun 07 21:22:18 1999 +0200
@@ -116,6 +116,9 @@
 * HOL/recdef (TFL): requires theory Recdef; 'congs' syntax now expects
 comma separated list of theorem names rather than an ML expression;
 
+* reset HOL_quantifiers by default, i.e. quantifiers are printed as
+ALL/EX rather than !/?;
+
 
 *** ZF ***
 
diff -r ac367328b875 -r 35f214e73668 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Jun 07 19:25:12 1999 +0200
+++ b/src/HOL/HOL.thy	Mon Jun 07 21:22:18 1999 +0200
@@ -212,7 +212,7 @@
 
 (** Choice between the HOL and Isabelle style of quantifiers **)
 
-val HOL_quantifiers = ref true;
+val HOL_quantifiers = ref false;
 
 fun alt_ast_tr' (name, alt_name) =
   let