--- a/src/HOL/Hoare/Examples.ML Mon Mar 13 15:42:19 2000 +0100
+++ b/src/HOL/Hoare/Examples.ML Mon Mar 13 16:23:34 2000 +0100
@@ -50,7 +50,7 @@
\ OD \
\ {c = A^B}";
by (hoare_tac (Asm_full_simp_tac) 1);
-by (cases_tac "b" 1);
+by (case_tac "b" 1);
by (hyp_subst_tac 1);
by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
by (asm_simp_tac (simpset() addsimps [mult_assoc]) 1);
@@ -67,7 +67,7 @@
\ {b = fac A}";
by (hoare_tac Asm_full_simp_tac 1);
by (Clarify_tac 1);
-by (cases_tac "a" 1);
+by (case_tac "a" 1);
by (ALLGOALS
(asm_simp_tac
(simpset() addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc])));