src/HOL/HOL.thy
changeset 14357 e49d5d5ae66a
parent 14295 7f115e5c5de4
child 14361 ad2f5da643b4
     1.1 --- a/src/HOL/HOL.thy	Wed Jan 14 04:41:16 2004 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Jan 14 07:53:27 2004 +0100
     1.3 @@ -969,4 +969,26 @@
     1.4   "ALL x<=y. P"  =>  "ALL x. x <= y --> P"
     1.5   "EX x<=y. P"   =>  "EX x. x <= y & P"
     1.6  
     1.7 +print_translation {*
     1.8 +let
     1.9 +  fun all_tr' [Const ("_bound",_) $ Free (v,_), 
    1.10 +               Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
    1.11 +  (if v=v' then Syntax.const "_lessAll" $ Syntax.mark_bound v' $ n $ P else raise Match)
    1.12 +
    1.13 +  | all_tr' [Const ("_bound",_) $ Free (v,_), 
    1.14 +               Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
    1.15 +  (if v=v' then Syntax.const "_leAll" $ Syntax.mark_bound v' $ n $ P else raise Match);
    1.16 +
    1.17 +  fun ex_tr' [Const ("_bound",_) $ Free (v,_), 
    1.18 +               Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
    1.19 +  (if v=v' then Syntax.const "_lessEx" $ Syntax.mark_bound v' $ n $ P else raise Match)
    1.20 +
    1.21 +  | ex_tr' [Const ("_bound",_) $ Free (v,_), 
    1.22 +               Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
    1.23 +  (if v=v' then Syntax.const "_leEx" $ Syntax.mark_bound v' $ n $ P else raise Match)
    1.24 +in
    1.25 +[("ALL ", all_tr'), ("EX ", ex_tr')]
    1.26  end
    1.27 +*}
    1.28 +
    1.29 +end