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/Metis_Examples/Binary_Tree.thy
changeset 45502 6246bef495ff
parent 43197 c71657bbdbc0
child 45705 a25ff4283352 
--- a/src/HOL/Metis_Examples/Binary_Tree.thy	Tue Nov 15 09:22:19 2011 +0100
+++ b/src/HOL/Metis_Examples/Binary_Tree.thy	Tue Nov 15 12:39:29 2011 +0100
@@ -264,7 +264,7 @@
      "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2"
 apply (induct t1)
  apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
-              semiring_norm(111))
+              Suc_eq_plus1)
 by (simp add: left_distrib)
 
 declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]]
isabelle