--- a/src/HOL/Induct/Mutil.ML Sat Mar 04 11:42:12 2000 +0100
+++ b/src/HOL/Induct/Mutil.ML Sat Mar 04 11:52:42 2000 +0100
@@ -48,7 +48,6 @@
by (subgoal_tac (*seems the easiest way of turning one to the other*)
"({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \
\ {(i, n+n), (i, Suc(n+n))}" 1);
-by (Blast_tac 2);
by (asm_simp_tac (simpset() addsimps [domino.horiz]) 1);
by Auto_tac;
qed "dominoes_tile_row";
--- a/src/HOL/ex/BT.ML Sat Mar 04 11:42:12 2000 +0100
+++ b/src/HOL/ex/BT.ML Sat Mar 04 11:52:42 2000 +0100
@@ -10,23 +10,23 @@
Goal "n_leaves(reflect(t)) = n_leaves(t)";
by (induct_tac "t" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute])));
+by Auto_tac;
qed "n_leaves_reflect";
Goal "n_nodes(reflect(t)) = n_nodes(t)";
by (induct_tac "t" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute])));
+by Auto_tac;
qed "n_nodes_reflect";
(*The famous relationship between the numbers of leaves and nodes*)
Goal "n_leaves(t) = Suc(n_nodes(t))";
by (induct_tac "t" 1);
-by (ALLGOALS Asm_simp_tac);
+by Auto_tac;
qed "n_leaves_nodes";
Goal "reflect(reflect(t))=t";
by (induct_tac "t" 1);
-by (ALLGOALS Asm_simp_tac);
+by Auto_tac;
qed "reflect_reflect_ident";
Goal "bt_map f (reflect t) = reflect (bt_map f t)";
--- a/src/HOL/ex/BT.thy Sat Mar 04 11:42:12 2000 +0100
+++ b/src/HOL/ex/BT.thy Sat Mar 04 11:52:42 2000 +0100
@@ -6,9 +6,10 @@
Binary trees (based on the ZF version)
*)
-BT = List +
+BT = Main +
-datatype 'a bt = Lf | Br 'a ('a bt) ('a bt)
+datatype 'a bt = Lf
+ | Br 'a ('a bt) ('a bt)
consts
n_nodes :: 'a bt => nat