# HG changeset patch
# User nipkow
# Date 878540894 -3600
# Node ID d6d06a03a2e9fe9a30cc38986e1cb3fd276e41d0
# Parent  99224854a0ac2966eec140f0323fe96760b5a0b7
expand_list_case -> split_list_case

diff -r 99224854a0ac -r d6d06a03a2e9 src/HOL/List.ML
--- a/src/HOL/List.ML	Sun Nov 02 14:01:38 1997 +0100
+++ b/src/HOL/List.ML	Mon Nov 03 08:08:14 1997 +0100
@@ -48,8 +48,6 @@
 
 (** list_case **)
 
-val expand_list_case = split_list_case;
-
 val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
 by (induct_tac "xs" 1);
 by (REPEAT(resolve_tac prems 1));
@@ -197,17 +195,17 @@
 
 goal thy "!!xs. xs ~= [] ==> hd(xs @ ys) = hd xs";
 by (asm_simp_tac (!simpset addsimps [hd_append]
-                           addsplits [expand_list_case]) 1);
+                           addsplits [split_list_case]) 1);
 qed "hd_append2";
 Addsimps [hd_append2];
 
 goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
-by (simp_tac (!simpset addsplits [expand_list_case]) 1);
+by (simp_tac (!simpset addsplits [split_list_case]) 1);
 qed "tl_append";
 
 goal thy "!!xs. xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys";
 by (asm_simp_tac (!simpset addsimps [tl_append]
-                           addsplits [expand_list_case]) 1);
+                           addsplits [split_list_case]) 1);
 qed "tl_append2";
 Addsimps [tl_append2];
 
diff -r 99224854a0ac -r d6d06a03a2e9 src/HOL/ex/Sorting.ML
--- a/src/HOL/ex/Sorting.ML	Sun Nov 02 14:01:38 1997 +0100
+++ b/src/HOL/ex/Sorting.ML	Mon Nov 03 08:08:14 1997 +0100
@@ -30,7 +30,7 @@
 val prems = goalw Sorting.thy [transf_def]
   "transf(le) ==> sorted1 le xs = sorted le xs";
 by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_list_case])));
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [split_list_case])));
 by (cut_facts_tac prems 1);
 by (Fast_tac 1);
 qed "sorted1_is_sorted";
diff -r 99224854a0ac -r d6d06a03a2e9 src/HOLCF/IOA/ABP/Correctness.ML
--- a/src/HOLCF/IOA/ABP/Correctness.ML	Sun Nov 02 14:01:38 1997 +0100
+++ b/src/HOLCF/IOA/ABP/Correctness.ML	Mon Nov 03 08:08:14 1997 +0100
@@ -49,7 +49,7 @@
  by (List.list.induct_tac "l" 1);
  by (Simp_tac 1);
  by (Simp_tac 1);
- by (rtac (expand_list_case RS iffD2) 1);
+ by (rtac (split_list_case RS iffD2) 1);
  by (Asm_full_simp_tac 1);
  by (REPEAT (rtac allI 1)); 
  by (rtac impI 1); 
@@ -68,7 +68,7 @@
 by (rotate 1 1);
 by (asm_full_simp_tac list_ss 1);
 by (Simp_tac 1);
-by (rtac (expand_list_case RS iffD2) 1);
+by (rtac (split_list_case RS iffD2) 1);
 by (asm_full_simp_tac list_ss 1);
 by (REPEAT (rtac allI 1)); 
  by (rtac impI 1); 
@@ -100,7 +100,7 @@
 goal Correctness.thy "!!l.[| l~=[] |] ==>   \
 \   hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))";
  by (Simp_tac 1);
- by (rtac (expand_list_case RS iffD2) 1);
+ by (rtac (split_list_case RS iffD2) 1);
  by (asm_full_simp_tac list_ss 1);
  by (REPEAT (rtac allI 1)); 
  by (rtac impI 1);