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/Tools/SMT/smt_normalize.ML
changeset 47207 9368aa814518
parent 47155 ade3fc826af3
child 50601 74da81de127f 
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu Mar 29 14:47:31 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Mar 30 08:10:28 2012 +0200
@@ -467,7 +467,7 @@
     let
       val eq = SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
       val ss = HOL_ss
-        addsimps [@{thm Nat_Numeral.int_numeral}]
+        addsimps [@{thm Int.int_numeral}]
       fun tac _ = Simplifier.simp_tac (Simplifier.context ctxt ss) 1       
     in Goal.norm_result (Goal.prove_internal [] eq tac) end
isabelle