print translation for ALL x <= n. P x

--- a/doc-src/TutorialI/Types/Overloading2.thy	Wed Jan 14 04:41:16 2004 +0100
+++ b/doc-src/TutorialI/Types/Overloading2.thy	Wed Jan 14 07:53:27 2004 +0100
@@ -32,14 +32,12 @@
 defined on all numeric types and sometimes on other types as well, for example
 $-$ and @{text"\<le>"} on sets.
 
-In addition there is a special input syntax for bounded quantifiers:
+In addition there is a special syntax for bounded quantifiers:
 \begin{center}
 \begin{tabular}{lcl}
-@{text"\<forall>x \<le> y. P x"} & @{text"\<rightharpoonup>"} & @{prop"\<forall>x. x \<le> y \<longrightarrow> P x"} \\
-@{text"\<exists>x \<le> y. P x"} & @{text"\<rightharpoonup>"} & @{prop"\<exists>x. x \<le> y \<and> P x"}
+@{prop"\<forall>x \<le> y. P x"} & @{text"\<rightleftharpoons>"} & @{prop [source] "\<forall>x. x \<le> y \<longrightarrow> P x"} \\
+@{prop"\<exists>x \<le> y. P x"} & @{text"\<rightleftharpoons>"} & @{prop [source] "\<exists>x. x \<le> y \<and> P x"}
 \end{tabular}
 \end{center}
 And analogously for @{text"<"} instead of @{text"\<le>"}.
-The form on the left is translated into the one on the right upon input.
-For technical reasons, it is not translated back upon output.
 *}(*<*)end(*>*)

--- 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