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 49962 a8cc904a6820
parent 45705 a25ff4283352
child 50705 0e943b33d907 
--- a/src/HOL/Metis_Examples/Binary_Tree.thy	Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Metis_Examples/Binary_Tree.thy	Fri Oct 19 15:12:52 2012 +0200
@@ -223,7 +223,7 @@
 apply (induct t1)
  apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
               Suc_eq_plus1)
-by (simp add: left_distrib)
+by (simp add: distrib_right)
 
 lemma (*bt_map_append:*)
      "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)"
isabelle