--- 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];
--- 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";
--- 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);