Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Import/HOL/HOL4Word32.thy
changeset 26086 3c243098b64a
parent 25919 8b1c0d434824
child 30952 7ab2716dd93b 
--- a/src/HOL/Import/HOL/HOL4Word32.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Import/HOL/HOL4Word32.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -117,9 +117,8 @@
      (op <::nat => nat => bool) (0::nat)
       ((op ^::nat => nat => nat)
         ((number_of \<Colon> int => nat)
-          ((op BIT \<Colon> int => bit => int)
-            ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-            (bit.B0::bit)))
+          ((Int.Bit0 \<Colon> int => int)
+            ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
         n))"
   by (import bits ZERO_LT_TWOEXP)
 
@@ -137,17 +136,13 @@
            ((op <::nat => nat => bool)
              ((op ^::nat => nat => nat)
                ((number_of \<Colon> int => nat)
-                 ((op BIT \<Colon> int => bit => int)
-                   ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                     (bit.B1::bit))
-                   (bit.B0::bit)))
+                 ((Int.Bit0 \<Colon> int => int)
+                   ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
                a)
              ((op ^::nat => nat => nat)
                ((number_of \<Colon> int => nat)
-                 ((op BIT \<Colon> int => bit => int)
-                   ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                     (bit.B1::bit))
-                   (bit.B0::bit)))
+                 ((Int.Bit0 \<Colon> int => int)
+                   ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
                b))))"
   by (import bits TWOEXP_MONO)
 
@@ -159,17 +154,13 @@
            ((op <=::nat => nat => bool)
              ((op ^::nat => nat => nat)
                ((number_of \<Colon> int => nat)
-                 ((op BIT \<Colon> int => bit => int)
-                   ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                     (bit.B1::bit))
-                   (bit.B0::bit)))
+                 ((Int.Bit0 \<Colon> int => int)
+                   ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
                a)
              ((op ^::nat => nat => nat)
                ((number_of \<Colon> int => nat)
-                 ((op BIT \<Colon> int => bit => int)
-                   ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                     (bit.B1::bit))
-                   (bit.B0::bit)))
+                 ((Int.Bit0 \<Colon> int => int)
+                   ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
                b))))"
   by (import bits TWOEXP_MONO2)
 
@@ -180,17 +171,13 @@
           (op <=::nat => nat => bool)
            ((op ^::nat => nat => nat)
              ((number_of \<Colon> int => nat)
-               ((op BIT \<Colon> int => bit => int)
-                 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                   (bit.B1::bit))
-                 (bit.B0::bit)))
+               ((Int.Bit0 \<Colon> int => int)
+                 ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
              ((op -::nat => nat => nat) a b))
            ((op ^::nat => nat => nat)
              ((number_of \<Colon> int => nat)
-               ((op BIT \<Colon> int => bit => int)
-                 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                   (bit.B1::bit))
-                 (bit.B0::bit)))
+               ((Int.Bit0 \<Colon> int => int)
+                 ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
              a)))"
   by (import bits EXP_SUB_LESS_EQ)
 
@@ -349,25 +336,19 @@
                  (op =::nat => nat => bool)
                   ((op ^::nat => nat => nat)
                     ((number_of \<Colon> int => nat)
-                      ((op BIT \<Colon> int => bit => int)
-                        ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                          (bit.B1::bit))
-                        (bit.B0::bit)))
+                      ((Int.Bit0 \<Colon> int => int)
+                        ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
                     b)
                   ((op *::nat => nat => nat)
                     ((op ^::nat => nat => nat)
                       ((number_of \<Colon> int => nat)
-                        ((op BIT \<Colon> int => bit => int)
-                          ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                            (bit.B1::bit))
-                          (bit.B0::bit)))
+                        ((Int.Bit0 \<Colon> int => int)
+                          ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
                       ((op +::nat => nat => nat) x (1::nat)))
                     ((op ^::nat => nat => nat)
                       ((number_of \<Colon> int => nat)
-                        ((op BIT \<Colon> int => bit => int)
-                          ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                            (bit.B1::bit))
-                          (bit.B0::bit)))
+                        ((Int.Bit0 \<Colon> int => int)
+                          ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
                       a))))))"
   by (import bits LESS_EXP_MULT2)
isabelle