--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Fri Mar 10 23:04:07 2000 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Mon Mar 13 09:08:27 2000 +0100
@@ -857,9 +857,9 @@
\ --> seq_take n`(x @@ (t>>y1)) = seq_take n`(x @@ (t>>y2)))";
by (Seq_induct_tac "x" [] 1);
by (strip_tac 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by Auto_tac;
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by Auto_tac;
qed"take_reduction1";
@@ -879,9 +879,9 @@
\ --> seq_take n`(x @@ (t>>y1)) << seq_take n`(x @@ (t>>y2)))";
by (Seq_induct_tac "x" [] 1);
by (strip_tac 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by Auto_tac;
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by Auto_tac;
qed"take_reduction_less1";
--- 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),