--- a/src/HOLCF/ex/Hoare.ML Fri Mar 10 23:04:07 2000 +0100
+++ b/src/HOLCF/ex/Hoare.ML Mon Mar 13 09:08:27 2000 +0100
@@ -183,7 +183,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (exhaust_tac "k" 1),
+ (cases_tac "k" 1),
(hyp_subst_tac 1),
(Simp_tac 1),
(strip_tac 1),
@@ -220,7 +220,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (exhaust_tac "k" 1),
+ (cases_tac "k" 1),
(hyp_subst_tac 1),
(Simp_tac 1),
(strip_tac 1),
@@ -381,7 +381,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (exhaust_tac "k" 1),
+ (cases_tac "k" 1),
(hyp_subst_tac 1),
(strip_tac 1),
(Simp_tac 1),
@@ -410,7 +410,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (exhaust_tac "k" 1),
+ (cases_tac "k" 1),
(hyp_subst_tac 1),
(Simp_tac 1),
(strip_tac 1),