--- a/src/HOL/Power.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Power.ML Mon Mar 13 12:51:10 2000 +0100
@@ -48,7 +48,7 @@
(*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***)
Goal "(n choose 0) = 1";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (ALLGOALS Asm_simp_tac);
qed "binomial_n_0";
@@ -99,7 +99,7 @@
by (induct_tac "n" 1);
by (simp_tac (simpset() addsimps [binomial_0]) 1);
by (Clarify_tac 1);
-by (exhaust_tac "k" 1);
+by (cases_tac "k" 1);
by (auto_tac (claset(),
simpset() addsimps [add_mult_distrib, add_mult_distrib2,
le_Suc_eq, binomial_eq_0]));