--- a/src/HOL/HOL.thy Wed Jan 14 04:41:16 2004 +0100
+++ b/src/HOL/HOL.thy Wed Jan 14 07:53:27 2004 +0100
@@ -969,4 +969,26 @@
"ALL x<=y. P" => "ALL x. x <= y --> P"
"EX x<=y. P" => "EX x. x <= y & P"
+print_translation {*
+let
+ fun all_tr' [Const ("_bound",_) $ Free (v,_),
+ Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
+ (if v=v' then Syntax.const "_lessAll" $ Syntax.mark_bound v' $ n $ P else raise Match)
+
+ | all_tr' [Const ("_bound",_) $ Free (v,_),
+ Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
+ (if v=v' then Syntax.const "_leAll" $ Syntax.mark_bound v' $ n $ P else raise Match);
+
+ fun ex_tr' [Const ("_bound",_) $ Free (v,_),
+ Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
+ (if v=v' then Syntax.const "_lessEx" $ Syntax.mark_bound v' $ n $ P else raise Match)
+
+ | ex_tr' [Const ("_bound",_) $ Free (v,_),
+ Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
+ (if v=v' then Syntax.const "_leEx" $ Syntax.mark_bound v' $ n $ P else raise Match)
+in
+[("ALL ", all_tr'), ("EX ", ex_tr')]
end
+*}
+
+end