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.
Numeral.mk_cnumber;
authorwenzelm
Thu, 05 Jul 2007 00:06:09 +0200
changeset 23572 b3ce27bd211f
parent 23571 0cd175710a93
child 23573 d85a277f90fd
Numeral.mk_cnumber;
src/HOL/Arith_Tools.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Arith_Tools.thy	Wed Jul 04 21:20:23 2007 +0200
+++ b/src/HOL/Arith_Tools.thy	Thu Jul 05 00:06:09 2007 +0200
@@ -591,11 +591,11 @@
 
 fun mk_const phi cT x =
  let val (a, b) = Rat.quotient_of_rat x
- in if b = 1 then Normalizer.mk_cnumber cT a
+ in if b = 1 then Numeral.mk_cnumber cT a
     else Thm.capply
          (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
-                     (Normalizer.mk_cnumber cT a))
-         (Normalizer.mk_cnumber cT b)
+                     (Numeral.mk_cnumber cT a))
+         (Numeral.mk_cnumber cT b)
   end
 
 in
@@ -723,11 +723,11 @@
 
 fun mk_frac phi cT x =
  let val (a, b) = Rat.quotient_of_rat x
- in if b = 1 then Normalizer.mk_cnumber cT a
+ in if b = 1 then Numeral.mk_cnumber cT a
     else Thm.capply
          (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
-                     (Normalizer.mk_cnumber cT a))
-         (Normalizer.mk_cnumber cT b)
+                     (Numeral.mk_cnumber cT a))
+         (Numeral.mk_cnumber cT b)
  end
 
 fun whatis x ct = case term_of ct of
isabelle