--- a/src/HOL/Integ/NatBin.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Integ/NatBin.ML Mon Mar 13 12:51:10 2000 +0100
@@ -319,17 +319,17 @@
(* These two can be useful when m = number_of... *)
Goal "(m::nat) + n = (if m=#0 then n else Suc ((m - #1) + n))";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
by (ALLGOALS (asm_simp_tac numeral_ss));
qed "add_eq_if";
Goal "(m::nat) * n = (if m=#0 then #0 else n + ((m - #1) * n))";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
by (ALLGOALS (asm_simp_tac numeral_ss));
qed "mult_eq_if";
Goal "(p ^ m :: nat) = (if m=#0 then #1 else p * (p ^ (m - #1)))";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
by (ALLGOALS (asm_simp_tac numeral_ss));
qed "power_eq_if";