# HG changeset patch
# User wenzelm
# Date 934920803 -7200
# Node ID 36e58620ffc8352b5cbd12023624f9ec29bf4f18
# Parent  2919daadba912f8887681cf0432720d848512c3e
replaced HOL_quantifiers flag by "HOL" print mode;
simplified HOL basic syntax (more orthogonal);

diff -r 2919daadba91 -r 36e58620ffc8 NEWS
--- a/NEWS	Tue Aug 17 22:11:05 1999 +0200
+++ b/NEWS	Tue Aug 17 22:13:23 1999 +0200
@@ -147,18 +147,15 @@
 
 ** HOL misc **
 
-* HOL/datatype: Now also handles arbitrarily branching datatypes
-  (using function types) such as
-
-  datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
-
 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
 -- avoids syntactic ambiguities and treats state, transition, and
 temporal levels more uniformly; introduces INCOMPATIBILITIES due to
 changed syntax and (many) tactics;
 
-* New bounded quantifier syntax (input only):
-  ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P
+* HOL/datatype: Now also handles arbitrarily branching datatypes
+  (using function types) such as
+
+  datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
 
 * HOL/typedef: fixed type inference for representing set; type
 arguments now have to occur explicitly on the rhs as type constraints;
@@ -170,6 +167,17 @@
 INCOMPATIBILITY: while [] and infix # syntax is still there, of
 course, ML tools referring to List.list.op # etc. have to be adapted;
 
+* HOL_quantifiers flag superseded by "HOL" print mode, which is
+disabled by default; run isabelle with option -m HOL to get back to
+the original Gordon/HOL-style output;
+
+* HOL/Ord.thy: new bounded quantifier syntax (input only): ALL x<y. P,
+ALL x<=y. P, EX x<y. P, EX x<=y. P;
+
+* HOL basic syntax simplified (more orthogonal): all variants of
+All/Ex now support plain / symbolic / HOL notation; plain syntax for
+Eps operator is provided as well: "SOME x. P[x]";
+
 
 *** LK ***
 
diff -r 2919daadba91 -r 36e58620ffc8 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Aug 17 22:11:05 1999 +0200
+++ b/src/HOL/HOL.thy	Tue Aug 17 22:13:23 1999 +0200
@@ -40,9 +40,9 @@
   (* Binders *)
 
   Eps           :: ('a => bool) => 'a
-  All           :: ('a => bool) => bool             (binder "! " 10)
-  Ex            :: ('a => bool) => bool             (binder "? " 10)
-  Ex1           :: ('a => bool) => bool             (binder "?! " 10)
+  All           :: ('a => bool) => bool             (binder "ALL " 10)
+  Ex            :: ('a => bool) => bool             (binder "EX " 10)
+  Ex1           :: ('a => bool) => bool             (binder "EX! " 10)
   Let           :: ['a, 'a => 'b] => 'b
 
   (* Infixes *)
@@ -75,6 +75,7 @@
   (*See Nat.thy for "^"*)
 
 
+
 (** Additional concrete syntax **)
 
 nonterminals
@@ -82,16 +83,8 @@
   case_syn  cases_syn
 
 syntax
-
   "~="          :: ['a, 'a] => bool                 (infixl 50)
-
-  "@Eps"        :: [pttrn, bool] => 'a              ("(3@ _./ _)" [0, 10] 10)
-
-  (* Alternative Quantifiers *)
-
-  "*All"        :: [idts, bool] => bool             ("(3ALL _./ _)" [0, 10] 10)
-  "*Ex"         :: [idts, bool] => bool             ("(3EX _./ _)" [0, 10] 10)
-  "*Ex1"        :: [idts, bool] => bool             ("(3EX! _./ _)" [0, 10] 10)
+  "_Eps"        :: [pttrn, bool] => 'a              ("(3SOME _./ _)" [0, 10] 10)
 
   (* Let expressions *)
 
@@ -108,11 +101,8 @@
   "@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ | _")
 
 translations
-  "x ~= y"      == "~ (x = y)"
-  "@ x. b"      == "Eps (%x. b)"
-  "ALL xs. P"   => "! xs. P"
-  "EX xs. P"    => "? xs. P"
-  "EX! xs. P"   => "?! xs. P"
+  "x ~= y"                == "~ (x = y)"
+  "SOME x. P"             == "Eps (%x. P)"
   "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
   "let x = a in e"        == "Let a (%x. e)"
 
@@ -127,18 +117,15 @@
   "op -->"      :: [bool, bool] => bool             (infixr "\\<midarrow>\\<rightarrow>" 25)
   "op o"        :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl "\\<circ>" 55)
   "op ~="       :: ['a, 'a] => bool                 (infixl "\\<noteq>" 50)
-  "@Eps"        :: [pttrn, bool] => 'a              ("(3\\<epsilon>_./ _)" [0, 10] 10)
-  "! "          :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
-  "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
-  "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
+  "_Eps"        :: [pttrn, bool] => 'a              ("(3\\<epsilon>_./ _)" [0, 10] 10)
+  "ALL "        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
+  "EX "         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
+  "EX! "        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
   "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<Rightarrow>/ _)" 10)
 (*"@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ \\<orelse> _")*)
 
 syntax (symbols output)
   "op ~="       :: ['a, 'a] => bool                 ("(_ \\<noteq>/ _)" [51, 51] 50)
-  "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
-  "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
-  "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
 
 syntax (xsymbols)
   "op -->"      :: [bool, bool] => bool             (infixr "\\<longrightarrow>" 25)
@@ -146,6 +133,13 @@
 syntax (HTML output)
   Not           :: bool => bool                     ("\\<not> _" [40] 40)
 
+syntax (HOL)
+  "_Eps"        :: [pttrn, bool] => 'a              ("(3@ _./ _)" [0, 10] 10)
+  "ALL "        :: [idts, bool] => bool             ("(3! _./ _)" [0, 10] 10)
+  "EX "         :: [idts, bool] => bool             ("(3? _./ _)" [0, 10] 10)
+  "EX! "        :: [idts, bool] => bool             ("(3?! _./ _)" [0, 10] 10)
+
+
 
 (** Rules and definitions **)
 
@@ -205,24 +199,3 @@
 
 
 end
-
-
-ML
-
-
-(** Choice between the HOL and Isabelle style of quantifiers **)
-
-val HOL_quantifiers = ref true;
-
-fun alt_ast_tr' (name, alt_name) =
-  let
-    fun ast_tr' (*name*) args =
-      if ! HOL_quantifiers then raise Match
-      else Syntax.mk_appl (Syntax.Constant alt_name) args;
-  in
-    (name, ast_tr')
-  end;
-
-
-val print_ast_translation =
-  map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
diff -r 2919daadba91 -r 36e58620ffc8 src/HOL/Ord.thy
--- a/src/HOL/Ord.thy	Tue Aug 17 22:11:05 1999 +0200
+++ b/src/HOL/Ord.thy	Tue Aug 17 22:13:23 1999 +0200
@@ -56,16 +56,32 @@
 axclass linorder < order
   linorder_linear "x <= y | y <= x"
 
-(*bounded quantifiers*)
+
+(* bounded quantifiers *)
+
 syntax
-  "@lessAll" :: [idt, 'a, bool] => bool   ("(3! _<_./ _)"  [0, 0, 10] 10)
-  "@lessEx"  :: [idt, 'a, bool] => bool   ("(3? _<_./ _)"  [0, 0, 10] 10)
-  "@leAll"   :: [idt, 'a, bool] => bool   ("(3! _<=_./ _)" [0, 0, 10] 10)
-  "@leEx"    :: [idt, 'a, bool] => bool   ("(3? _<=_./ _)" [0, 0, 10] 10)
+  "_lessAll" :: [idt, 'a, bool] => bool   ("(3ALL _<_./ _)"  [0, 0, 10] 10)
+  "_lessEx"  :: [idt, 'a, bool] => bool   ("(3EX _<_./ _)"  [0, 0, 10] 10)
+  "_leAll"   :: [idt, 'a, bool] => bool   ("(3ALL _<=_./ _)" [0, 0, 10] 10)
+  "_leEx"    :: [idt, 'a, bool] => bool   ("(3EX _<=_./ _)" [0, 0, 10] 10)
+
+syntax (symbols)
+  "_lessAll" :: [idt, 'a, bool] => bool   ("(3\\<forall>_<_./ _)"  [0, 0, 10] 10)
+  "_lessEx"  :: [idt, 'a, bool] => bool   ("(3\\<exists>_<_./ _)"  [0, 0, 10] 10)
+  "_leAll"   :: [idt, 'a, bool] => bool   ("(3\\<forall>_<=_./ _)" [0, 0, 10] 10)
+  "_leEx"    :: [idt, 'a, bool] => bool   ("(3\\<exists>_<=_./ _)" [0, 0, 10] 10)
+
+syntax (HOL)
+  "_lessAll" :: [idt, 'a, bool] => bool   ("(3! _<_./ _)"  [0, 0, 10] 10)
+  "_lessEx"  :: [idt, 'a, bool] => bool   ("(3? _<_./ _)"  [0, 0, 10] 10)
+  "_leAll"   :: [idt, 'a, bool] => bool   ("(3! _<=_./ _)" [0, 0, 10] 10)
+  "_leEx"    :: [idt, 'a, bool] => bool   ("(3? _<=_./ _)" [0, 0, 10] 10)
+
 translations
- "! x<y.  P"  =>  "! x. x < y  --> P"
- "! x<=y. P"  =>  "! x. x <= y --> P"
- "? x<y.  P"  =>  "? x. x < y  & P"
- "? x<=y. P"  =>  "? x. x <= y & P"
+ "ALL x<y. P"   =>  "ALL x. x < y --> P"
+ "EX x<y. P"    =>  "EX x. x < y  & P"
+ "ALL x<=y. P"  =>  "ALL x. x <= y --> P"
+ "EX x<=y. P"   =>  "EX x. x <= y & P"
+
 
 end
diff -r 2919daadba91 -r 36e58620ffc8 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Aug 17 22:11:05 1999 +0200
+++ b/src/HOL/Set.thy	Tue Aug 17 22:13:23 1999 +0200
@@ -44,14 +44,13 @@
 
 syntax
 
-
   (* Infix syntax for non-membership *)
 
   "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
   "op ~:"       :: ['a, 'a set] => bool               ("(_/ ~: _)" [50, 51] 50)
 
+
   "@Finset"     :: args => 'a set                     ("{(_)}")
-
   "@Coll"       :: [pttrn, bool] => 'a set            ("(1{_./ _})")
   "@SetCompr"   :: ['a, idts, bool] => 'a set         ("(1{_ |/_./ _})")
 
@@ -64,11 +63,12 @@
   "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3UN _:_./ _)" 10)
 
   (* Bounded Quantifiers *)
+  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" [0, 0, 10] 10)
+  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" [0, 0, 10] 10)
 
-  "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3! _:_./ _)" [0, 0, 10] 10)
-  "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" [0, 0, 10] 10)
-  "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" [0, 0, 10] 10)
-  "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" [0, 0, 10] 10)
+syntax (HOL)
+  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3! _:_./ _)" [0, 0, 10] 10)
+  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" [0, 0, 10] 10)
 
 translations
   "range f"     == "f``UNIV"
@@ -78,14 +78,12 @@
   "{x. P}"      == "Collect (%x. P)"
   "UN x y. B"   == "UN x. UN y. B"
   "UN x. B"     == "UNION UNIV (%x. B)"
-  "INT x y. B"   == "INT x. INT y. B"
+  "INT x y. B"  == "INT x. INT y. B"
   "INT x. B"    == "INTER UNIV (%x. B)"
   "UN x:A. B"   == "UNION A (%x. B)"
   "INT x:A. B"  == "INTER A (%x. B)"
-  "! x:A. P"    == "Ball A (%x. P)"
-  "? x:A. P"    == "Bex A (%x. P)"
-  "ALL x:A. P"  => "Ball A (%x. P)"
-  "EX x:A. P"   => "Bex A (%x. P)"
+  "ALL x:A. P"  == "Ball A (%x. P)"
+  "EX x:A. P"   == "Bex A (%x. P)"
 
 syntax ("" output)
   "_setle"      :: ['a set, 'a set] => bool           ("op <=")
@@ -112,12 +110,8 @@
   "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Inter> _\\<in>_./ _)" 10)
   Union         :: (('a set) set) => 'a set           ("\\<Union> _" [90] 90)
   Inter         :: (('a set) set) => 'a set           ("\\<Inter> _" [90] 90)
-  "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
-  "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
-
-syntax (symbols output)
-  "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
-  "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
+  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
+  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
 
 translations
   "op \\<subseteq>" => "op <= :: [_ set, _ set] => bool"
@@ -138,7 +132,6 @@
 
 
 defs
-
   Ball_def      "Ball A P       == ! x. x:A --> P(x)"
   Bex_def       "Bex A P        == ? x. x:A & P(x)"
   subset_def    "A <= B         == ! x:A. x:B"
@@ -157,6 +150,7 @@
   insert_def    "insert a B     == {x. x=a} Un B"
   image_def     "f``A           == {y. ? x:A. y=f(x)}"
 
+
 end
 
 
@@ -178,7 +172,7 @@
 (* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P}      *)
 (* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *)
 
-val ex_tr = snd(mk_binder_tr("? ","Ex"));
+val ex_tr = snd(mk_binder_tr("EX ","Ex"));
 
 fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1
   | nvars(_) = 1;
@@ -208,7 +202,6 @@
 val parse_translation = [("@SetCompr", setcompr_tr)];
 val print_translation = [("Collect", setcompr_tr')];
 val typed_print_translation = [("op <=", le_tr'), ("op <", less_tr')];
-val print_ast_translation =
-  map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];
+
 
 end;