# HG changeset patch # User kleing # Date 1074063207 -3600 # Node ID e49d5d5ae66a1a410cc480b6d88467319ffd1e3b # Parent 9e3ce012f8430174b4a90b85ae61426e1c0135a5 print translation for ALL x <= n. P x diff -r 9e3ce012f843 -r e49d5d5ae66a doc-src/TutorialI/Types/Overloading2.thy --- 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"\"} 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"\x \ y. P x"} & @{text"\"} & @{prop"\x. x \ y \ P x"} \\ -@{text"\x \ y. P x"} & @{text"\"} & @{prop"\x. x \ y \ P x"} +@{prop"\x \ y. P x"} & @{text"\"} & @{prop [source] "\x. x \ y \ P x"} \\ +@{prop"\x \ y. P x"} & @{text"\"} & @{prop [source] "\x. x \ y \ P x"} \end{tabular} \end{center} And analogously for @{text"<"} instead of @{text"\"}. -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(*>*) diff -r 9e3ce012f843 -r e49d5d5ae66a src/HOL/HOL.thy --- 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