# HG changeset patch
# User wenzelm
# Date 952950649 -3600
# Node ID 17e62ef34ec8ee9086be50d7858f83768115fa98
# Parent  b8389b4fca9c42230145c3b75a0a0d04d45d38be
renamed cases_tac to case_tac;

diff -r b8389b4fca9c -r 17e62ef34ec8 src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Mon Mar 13 13:28:31 2000 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Mon Mar 13 13:30:49 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 (cases_tac "n" 1);
+by (case_tac "n" 1);
 by Auto_tac;
-by (cases_tac "n" 1);
+by (case_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 (cases_tac "n" 1);
+by (case_tac "n" 1);
 by Auto_tac;
-by (cases_tac "n" 1);
+by (case_tac "n" 1);
 by Auto_tac;
 qed"take_reduction_less1";
 
diff -r b8389b4fca9c -r 17e62ef34ec8 src/HOLCF/ex/Hoare.ML
--- a/src/HOLCF/ex/Hoare.ML	Mon Mar 13 13:28:31 2000 +0100
+++ b/src/HOLCF/ex/Hoare.ML	Mon Mar 13 13:30:49 2000 +0100
@@ -183,7 +183,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (cases_tac "k" 1),
+        (case_tac "k" 1),
         (hyp_subst_tac 1),
         (Simp_tac 1),
         (strip_tac 1),
@@ -220,7 +220,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (cases_tac "k" 1),
+        (case_tac "k" 1),
         (hyp_subst_tac 1),
         (Simp_tac 1),
         (strip_tac 1),
@@ -381,7 +381,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (cases_tac "k" 1),
+        (case_tac "k" 1),
         (hyp_subst_tac 1),
         (strip_tac 1),
         (Simp_tac 1),
@@ -410,7 +410,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (cases_tac "k" 1),
+        (case_tac "k" 1),
         (hyp_subst_tac 1),
         (Simp_tac 1),
         (strip_tac 1),