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/HOL4Real.thy
changeset 25919 8b1c0d434824
parent 20485 3078fd2eec7b
child 26086 3c243098b64a 
--- a/src/HOL/Import/HOL/HOL4Real.thy	Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Import/HOL/HOL4Real.thy	Tue Jan 15 16:19:23 2008 +0100
@@ -527,7 +527,7 @@
         ((op ^::real => nat => real) x
           ((number_of \<Colon> int => nat)
             ((op BIT \<Colon> int => bit => int)
-              ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+              ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
               (bit.B0::bit))))))"
   by (import real REAL_LE1_POW2)
 
@@ -539,7 +539,7 @@
         ((op ^::real => nat => real) x
           ((number_of \<Colon> int => nat)
             ((op BIT \<Colon> int => bit => int)
-              ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+              ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
               (bit.B0::bit))))))"
   by (import real REAL_LT1_POW2)
isabelle