added ALL print-translation for > and >=.
authornipkow
Thu Dec 02 11:59:34 2004 +0100 (2004-12-02)
changeset 15362a000b267be57
parent 15361 bb2dd95c8c5e
child 15363 885a40edcdba
added ALL print-translation for > and >=.
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Thu Dec 02 11:44:55 2004 +0100
     1.2 +++ b/src/HOL/HOL.thy	Thu Dec 02 11:59:34 2004 +0100
     1.3 @@ -1160,7 +1160,15 @@
     1.4  
     1.5    | all_tr' [Const ("_bound",_) $ Free (v,_), 
     1.6                 Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
     1.7 -  (if v=v' then Syntax.const "_leAll" $ Syntax.mark_bound v' $ n $ P else raise Match);
     1.8 +  (if v=v' then Syntax.const "_leAll" $ Syntax.mark_bound v' $ n $ P else raise Match)
     1.9 +
    1.10 +  | all_tr' [Const ("_bound",_) $ Free (v,_), 
    1.11 +               Const("op -->",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
    1.12 +  (if v=v' then Syntax.const "_gtAll" $ Syntax.mark_bound v' $ n $ P else raise Match)
    1.13 +
    1.14 +  | all_tr' [Const ("_bound",_) $ Free (v,_), 
    1.15 +               Const("op -->",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
    1.16 +  (if v=v' then Syntax.const "_geAll" $ Syntax.mark_bound v' $ n $ P else raise Match);
    1.17  
    1.18    fun ex_tr' [Const ("_bound",_) $ Free (v,_), 
    1.19                 Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
    1.20 @@ -1168,7 +1176,16 @@
    1.21  
    1.22    | ex_tr' [Const ("_bound",_) $ Free (v,_), 
    1.23                 Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
    1.24 -  (if v=v' then Syntax.const "_leEx" $ Syntax.mark_bound v' $ n $ P else raise Match)
    1.25 +  (if v=v' then Syntax.const "_leEx" $ Syntax.mark_bound v' $ n $ P else
    1.26 +               raise Match)
    1.27 +
    1.28 +  | ex_tr' [Const ("_bound",_) $ Free (v,_), 
    1.29 +               Const("op &",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
    1.30 +  (if v=v' then Syntax.const "_gtEx" $ Syntax.mark_bound v' $ n $ P else raise Match)
    1.31 +
    1.32 +  | ex_tr' [Const ("_bound",_) $ Free (v,_), 
    1.33 +               Const("op &",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
    1.34 +  (if v=v' then Syntax.const "_geEx" $ Syntax.mark_bound v' $ n $ P else raise Match)
    1.35  in
    1.36  [("ALL ", all_tr'), ("EX ", ex_tr')]
    1.37  end