# HG changeset patch
# User nipkow
# Date 952934907 -3600
# Node ID ae28c198e78d20e3ab23502b80ac7262d375e5ff
# Parent  8eb32cd3122eff687841b3b2a00a3139427f8aa2
exhaust->cases

diff -r 8eb32cd3122e -r ae28c198e78d src/HOLCF/IOA/meta_theory/Sequence.ML
--- 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";
 
diff -r 8eb32cd3122e -r ae28c198e78d src/HOLCF/ex/Hoare.ML
--- 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),