--- 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
--- 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)
--- 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)
--- 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)
--- 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)