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/Function/size.ML
changeset 35064 1bdef0c013d3
parent 35047 1b2bae06c796
child 35267 8dfd816713c6 
--- a/src/HOL/Tools/Function/size.ML	Tue Feb 09 11:07:14 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML	Tue Feb 09 11:47:47 2010 +0100
@@ -153,7 +153,7 @@
 
     val ctxt = ProofContext.init thy';
 
-    val simpset1 = HOL_basic_ss addsimps @{thm add_0} :: @{thm Nat.add_0_right} ::
+    val simpset1 = HOL_basic_ss addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} ::
       size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
     val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);
isabelle