old HOL syntax is for input only;
authorwenzelm
Sat Mar 05 19:58:56 2016 +0100 (2016-03-05)
changeset 625216383440f41a8
parent 62520 2382876c238b
child 62522 d32c23d29968
old HOL syntax is for input only;
NEWS
src/HOL/HOL.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Orderings.thy
src/HOL/Set.thy
     1.1 --- a/NEWS	Sat Mar 05 19:14:04 2016 +0100
     1.2 +++ b/NEWS	Sat Mar 05 19:58:56 2016 +0100
     1.3 @@ -23,6 +23,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@"
     1.8 +has been removed for output. It is retained for input only, until it is
     1.9 +eliminated altogether.
    1.10 +
    1.11  * (Co)datatype package:
    1.12    - the predicator :: ('a => bool) => 'a F => bool is now a first-class
    1.13      citizen in bounded natural functors
     2.1 --- a/src/HOL/HOL.thy	Sat Mar 05 19:14:04 2016 +0100
     2.2 +++ b/src/HOL/HOL.thy	Sat Mar 05 19:58:56 2016 +0100
     2.3 @@ -155,7 +155,7 @@
     2.4    Ex  (binder "EX " 10) and
     2.5    Ex1  (binder "EX! " 10)
     2.6  
     2.7 -notation (HOL)
     2.8 +notation (input)
     2.9    All  (binder "! " 10) and
    2.10    Ex  (binder "? " 10) and
    2.11    Ex1  (binder "?! " 10)
     3.1 --- a/src/HOL/Hilbert_Choice.thy	Sat Mar 05 19:14:04 2016 +0100
     3.2 +++ b/src/HOL/Hilbert_Choice.thy	Sat Mar 05 19:58:56 2016 +0100
     3.3 @@ -17,7 +17,7 @@
     3.4  
     3.5  syntax (epsilon)
     3.6    "_Eps"        :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
     3.7 -syntax (HOL)
     3.8 +syntax (input)
     3.9    "_Eps"        :: "[pttrn, bool] => 'a"    ("(3@ _./ _)" [0, 10] 10)
    3.10  syntax
    3.11    "_Eps"        :: "[pttrn, bool] => 'a"    ("(3SOME _./ _)" [0, 10] 10)
     4.1 --- a/src/HOL/Orderings.thy	Sat Mar 05 19:14:04 2016 +0100
     4.2 +++ b/src/HOL/Orderings.thy	Sat Mar 05 19:58:56 2016 +0100
     4.3 @@ -674,7 +674,7 @@
     4.4    "_All_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
     4.5    "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
     4.6  
     4.7 -syntax (HOL)
     4.8 +syntax (input)
     4.9    "_All_less" :: "[idt, 'a, bool] => bool"    ("(3! _<_./ _)"  [0, 0, 10] 10)
    4.10    "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3? _<_./ _)"  [0, 0, 10] 10)
    4.11    "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3! _<=_./ _)" [0, 0, 10] 10)
     5.1 --- a/src/HOL/Set.thy	Sat Mar 05 19:14:04 2016 +0100
     5.2 +++ b/src/HOL/Set.thy	Sat Mar 05 19:58:56 2016 +0100
     5.3 @@ -183,7 +183,7 @@
     5.4    "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3EX! _:_./ _)" [0, 0, 10] 10)
     5.5    "_Bleast"     :: "id => 'a set => bool => 'a"           ("(3LEAST _:_./ _)" [0, 0, 10] 10)
     5.6  
     5.7 -syntax (HOL)
     5.8 +syntax (input)
     5.9    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3! _:_./ _)" [0, 0, 10] 10)
    5.10    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3? _:_./ _)" [0, 0, 10] 10)
    5.11    "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3?! _:_./ _)" [0, 0, 10] 10)
    5.12 @@ -207,13 +207,6 @@
    5.13    "_setleEx"    :: "[idt, 'a, bool] => bool"  ("(3EX _<=_./ _)" [0, 0, 10] 10)
    5.14    "_setleEx1"   :: "[idt, 'a, bool] => bool"  ("(3EX! _<=_./ _)" [0, 0, 10] 10)
    5.15  
    5.16 -syntax (HOL output)
    5.17 -  "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)
    5.18 -  "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)
    5.19 -  "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3! _<=_./ _)" [0, 0, 10] 10)
    5.20 -  "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
    5.21 -  "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3?! _<=_./ _)" [0, 0, 10] 10)
    5.22 -
    5.23  syntax
    5.24    "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
    5.25    "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)