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/Library/comm_ring.ML
changeset 23261 85f27f79232f
parent 22997 d4f3b015b50b
child 24630 351a308ab58d 
--- a/src/HOL/Library/comm_ring.ML	Tue Jun 05 18:36:10 2007 +0200
+++ b/src/HOL/Library/comm_ring.ML	Tue Jun 05 19:19:30 2007 +0200
@@ -46,7 +46,7 @@
       in if i = 0
         then pol_PX T $ (pol_Pc T $ cring_one T)
           $ one $ (pol_Pc T $ cring_zero T)
-        else pol_Pinj T $ HOLogic.mk_nat (Intt.int i)
+        else pol_Pinj T $ HOLogic.mk_nat (Integer.int i)
           $ (pol_PX T $ (pol_Pc T $ cring_one T)
             $ one $ (pol_Pc T $ cring_zero T))
         end
isabelle