# 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\_./ _)" [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\_\_./ _)" [0, 0, 10] 10) "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [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\_\_./ _)" [0, 0, 10] 10) "_setlessEx" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10)