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/Arith_Tools.thy
changeset 23572 b3ce27bd211f
parent 23477 f4b83f03cac9
child 23881 851c74f1bb69 
--- 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