--- a/src/HOL/HOL.thy Thu Dec 02 11:09:19 2004 +0100
+++ b/src/HOL/HOL.thy Thu Dec 02 11:42:01 2004 +0100
@@ -1109,12 +1109,22 @@
"_leAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10)
"_leEx" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10)
+ "_gtAll" :: "[idt, 'a, bool] => bool" ("(3ALL _>_./ _)" [0, 0, 10] 10)
+ "_gtEx" :: "[idt, 'a, bool] => bool" ("(3EX _>_./ _)" [0, 0, 10] 10)
+ "_geAll" :: "[idt, 'a, bool] => bool" ("(3ALL _>=_./ _)" [0, 0, 10] 10)
+ "_geEx" :: "[idt, 'a, bool] => bool" ("(3EX _>=_./ _)" [0, 0, 10] 10)
+
syntax (xsymbols)
"_lessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10)
"_lessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10)
"_leAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
"_leEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
+ "_gtAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_>_./ _)" [0, 0, 10] 10)
+ "_gtEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_>_./ _)" [0, 0, 10] 10)
+ "_geAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
+ "_geEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
+
syntax (HOL)
"_lessAll" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10)
"_lessEx" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10)
@@ -1127,11 +1137,20 @@
"_leAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
"_leEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
+ "_gtAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_>_./ _)" [0, 0, 10] 10)
+ "_gtEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_>_./ _)" [0, 0, 10] 10)
+ "_geAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
+ "_geEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
+
translations
"ALL x<y. P" => "ALL x. x < y --> P"
"EX x<y. P" => "EX x. x < y & P"
"ALL x<=y. P" => "ALL x. x <= y --> P"
"EX x<=y. P" => "EX x. x <= y & P"
+ "ALL x>y. P" => "ALL x. x > y --> P"
+ "EX x>y. P" => "EX x. x > y & P"
+ "ALL x>=y. P" => "ALL x. x >= y --> P"
+ "EX x>=y. P" => "EX x. x >= y & P"
print_translation {*
let