Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reactivated translations for less/less_eq;
authorwenzelm
Sat, 13 May 2006 21:13:25 +0200
changeset 19637 d33a71ffb9e3
parent 19636 50515882049e
child 19638 4358b88a9d12
reactivated translations for less/less_eq;
src/HOL/Orderings.thy file | annotate | diff | comparison | revisions
src/HOL/Set.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Orderings.thy	Sat May 13 02:51:49 2006 +0200
+++ b/src/HOL/Orderings.thy	Sat May 13 21:13:25 2006 +0200
@@ -543,35 +543,35 @@
     if v=v' andalso not (v mem (map fst (Term.add_frees n [])))
     then Syntax.const q $ Syntax.mark_bound v' $ n $ P else raise Match;
   fun all_tr' [Const ("_bound",_) $ Free (v,_),
-               Const("op -->",_) $ (Const ("Orderings.less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
+               Const("op -->",_) $ (Const ("less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
     mk v v' "_lessAll" n P
 
   | all_tr' [Const ("_bound",_) $ Free (v,_),
-               Const("op -->",_) $ (Const ("Orderings.less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
+               Const("op -->",_) $ (Const ("less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
     mk v v' "_leAll" n P
 
   | all_tr' [Const ("_bound",_) $ Free (v,_),
-               Const("op -->",_) $ (Const ("Orderings.less",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
+               Const("op -->",_) $ (Const ("less",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
     mk v v' "_gtAll" n P
 
   | all_tr' [Const ("_bound",_) $ Free (v,_),
-               Const("op -->",_) $ (Const ("Orderings.less_eq",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
+               Const("op -->",_) $ (Const ("less_eq",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
     mk v v' "_geAll" n P;
 
   fun ex_tr' [Const ("_bound",_) $ Free (v,_),
-               Const("op &",_) $ (Const ("Orderings.less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
+               Const("op &",_) $ (Const ("less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
     mk v v' "_lessEx" n P
 
   | ex_tr' [Const ("_bound",_) $ Free (v,_),
-               Const("op &",_) $ (Const ("Orderings.less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
+               Const("op &",_) $ (Const ("less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
     mk v v' "_leEx" n P
 
   | ex_tr' [Const ("_bound",_) $ Free (v,_),
-               Const("op &",_) $ (Const ("Orderings.less",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
+               Const("op &",_) $ (Const ("less",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
     mk v v' "_gtEx" n P
 
   | ex_tr' [Const ("_bound",_) $ Free (v,_),
-               Const("op &",_) $ (Const ("Orderings.less_eq",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
+               Const("op &",_) $ (Const ("less_eq",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
     mk v v' "_geEx" n P
 in
 [("ALL ", all_tr'), ("EX ", ex_tr')]
--- a/src/HOL/Set.thy	Sat May 13 02:51:49 2006 +0200
+++ b/src/HOL/Set.thy	Sat May 13 21:13:25 2006 +0200
@@ -169,7 +169,7 @@
     fun less_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
           list_comb (Syntax.const "_setless", ts)
       | less_tr' _ _ _ = raise Match;
-  in [("Orderings.less_eq", le_tr'), ("Orderings.less", less_tr')] end
+  in [("less_eq", le_tr'), ("less", less_tr')] end
 *}
 
 
@@ -209,26 +209,26 @@
 let
   fun
     all_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
-             Const("op -->",_) $ (Const ("Orderings.less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
+             Const("op -->",_) $ (Const ("less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   (if v=v' andalso T="set"
    then Syntax.const "_setlessAll" $ Syntax.mark_bound v' $ n $ P
    else raise Match)
 
   | all_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
-             Const("op -->",_) $ (Const ("Orderings.less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
+             Const("op -->",_) $ (Const ("less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   (if v=v' andalso T="set"
    then Syntax.const "_setleAll" $ Syntax.mark_bound v' $ n $ P
    else raise Match);
 
   fun
     ex_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
-            Const("op &",_) $ (Const ("Orderings.less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
+            Const("op &",_) $ (Const ("less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   (if v=v' andalso T="set"
    then Syntax.const "_setlessEx" $ Syntax.mark_bound v' $ n $ P
    else raise Match)
 
   | ex_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
-            Const("op &",_) $ (Const ("Orderings.less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
+            Const("op &",_) $ (Const ("less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   (if v=v' andalso T="set"
    then Syntax.const "_setleEx" $ Syntax.mark_bound v' $ n $ P
    else raise Match)
isabelle