# HG changeset patch
# User wenzelm
# Date 1457204336 -3600
# Node ID 6383440f41a819b9b4b5fc863185378fa05d854e
# Parent  2382876c238b219e8c9362f2467be4d85d51c924
old HOL syntax is for input only;

diff -r 2382876c238b -r 6383440f41a8 NEWS
--- a/NEWS	Sat Mar 05 19:14:04 2016 +0100
+++ b/NEWS	Sat Mar 05 19:58:56 2016 +0100
@@ -23,6 +23,10 @@
 
 *** HOL ***
 
+* The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@"
+has been removed for output. It is retained for input only, until it is
+eliminated altogether.
+
 * (Co)datatype package:
   - the predicator :: ('a => bool) => 'a F => bool is now a first-class
     citizen in bounded natural functors
diff -r 2382876c238b -r 6383440f41a8 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Mar 05 19:14:04 2016 +0100
+++ b/src/HOL/HOL.thy	Sat Mar 05 19:58:56 2016 +0100
@@ -155,7 +155,7 @@
   Ex  (binder "EX " 10) and
   Ex1  (binder "EX! " 10)
 
-notation (HOL)
+notation (input)
   All  (binder "! " 10) and
   Ex  (binder "? " 10) and
   Ex1  (binder "?! " 10)
diff -r 2382876c238b -r 6383440f41a8 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sat Mar 05 19:14:04 2016 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Sat Mar 05 19:58:56 2016 +0100
@@ -17,7 +17,7 @@
 
 syntax (epsilon)
   "_Eps"        :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
-syntax (HOL)
+syntax (input)
   "_Eps"        :: "[pttrn, bool] => 'a"    ("(3@ _./ _)" [0, 10] 10)
 syntax
   "_Eps"        :: "[pttrn, bool] => 'a"    ("(3SOME _./ _)" [0, 10] 10)
diff -r 2382876c238b -r 6383440f41a8 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sat Mar 05 19:14:04 2016 +0100
+++ b/src/HOL/Orderings.thy	Sat Mar 05 19:58:56 2016 +0100
@@ -674,7 +674,7 @@
   "_All_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
   "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
 
-syntax (HOL)
+syntax (input)
   "_All_less" :: "[idt, 'a, bool] => bool"    ("(3! _<_./ _)"  [0, 0, 10] 10)
   "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3? _<_./ _)"  [0, 0, 10] 10)
   "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3! _<=_./ _)" [0, 0, 10] 10)
diff -r 2382876c238b -r 6383440f41a8 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Mar 05 19:14:04 2016 +0100
+++ b/src/HOL/Set.thy	Sat Mar 05 19:58:56 2016 +0100
@@ -183,7 +183,7 @@
   "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3EX! _:_./ _)" [0, 0, 10] 10)
   "_Bleast"     :: "id => 'a set => bool => 'a"           ("(3LEAST _:_./ _)" [0, 0, 10] 10)
 
-syntax (HOL)
+syntax (input)
   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3! _:_./ _)" [0, 0, 10] 10)
   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3? _:_./ _)" [0, 0, 10] 10)
   "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3?! _:_./ _)" [0, 0, 10] 10)
@@ -207,13 +207,6 @@
   "_setleEx"    :: "[idt, 'a, bool] => bool"  ("(3EX _<=_./ _)" [0, 0, 10] 10)
   "_setleEx1"   :: "[idt, 'a, bool] => bool"  ("(3EX! _<=_./ _)" [0, 0, 10] 10)
 
-syntax (HOL output)
-  "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)
-  "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)
-  "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3! _<=_./ _)" [0, 0, 10] 10)
-  "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
-  "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3?! _<=_./ _)" [0, 0, 10] 10)
-
 syntax
   "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
   "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)