src/HOL/Orderings.thy
changeset 62521 6383440f41a8
parent 61955 e96292f32c3c
child 63172 d4f459eb7ed0
     1.1 --- a/src/HOL/Orderings.thy	Sat Mar 05 19:14:04 2016 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Sat Mar 05 19:58:56 2016 +0100
     1.3 @@ -674,7 +674,7 @@
     1.4    "_All_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
     1.5    "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
     1.6  
     1.7 -syntax (HOL)
     1.8 +syntax (input)
     1.9    "_All_less" :: "[idt, 'a, bool] => bool"    ("(3! _<_./ _)"  [0, 0, 10] 10)
    1.10    "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3? _<_./ _)"  [0, 0, 10] 10)
    1.11    "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3! _<=_./ _)" [0, 0, 10] 10)