Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proof of n_leaves_reflect uses permutative rewriting.
authorlcp
Thu, 29 Jun 1995 16:39:24 +0200
changeset 1170 39119c4c7bac
parent 1169 5873833cf37f
child 1171 e4d6b42be73a
Proof of n_leaves_reflect uses permutative rewriting.
src/ZF/ex/BT.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/ex/BT.ML	Thu Jun 29 16:33:17 1995 +0200
+++ b/src/ZF/ex/BT.ML	Thu Jun 29 16:39:24 1995 +0200
@@ -129,8 +129,7 @@
 val prems = goal BT.thy
     "t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)";
 by (bt_ind_tac "t" prems 1);
-by (ALLGOALS (asm_simp_tac bt_ss));
-by (REPEAT (ares_tac [add_commute, n_leaves_type] 1));
+by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_commute, n_leaves_type])));
 qed "n_leaves_reflect";
 
 val prems = goal BT.thy
isabelle