Replaced res_inst-list_cases by generic exhaust_tac.
--- a/src/HOL/List.ML Thu May 22 09:20:28 1997 +0200
+++ b/src/HOL/List.ML Thu May 22 09:39:37 1997 +0200
@@ -294,10 +294,10 @@
by(nat_ind_tac "n" 1);
by(Asm_simp_tac 1);
br allI 1;
- by(res_inst_tac [("xs","xs")]list_cases 1);
+ by(exhaust_tac "xs" 1);
by(ALLGOALS Asm_simp_tac);
br allI 1;
-by(res_inst_tac [("xs","xs")]list_cases 1);
+by(exhaust_tac "xs" 1);
by(ALLGOALS Asm_simp_tac);
qed_spec_mp "nth_append";
@@ -365,7 +365,7 @@
by(nat_ind_tac "n" 1);
by(ALLGOALS Asm_simp_tac);
br allI 1;
-by(res_inst_tac [("xs","xs")]list_cases 1);
+by(exhaust_tac "xs" 1);
by(ALLGOALS Asm_simp_tac);
qed_spec_mp "length_take";
Addsimps [length_take];
@@ -374,7 +374,7 @@
by(nat_ind_tac "n" 1);
by(ALLGOALS Asm_simp_tac);
br allI 1;
-by(res_inst_tac [("xs","xs")]list_cases 1);
+by(exhaust_tac "xs" 1);
by(ALLGOALS Asm_simp_tac);
qed_spec_mp "length_drop";
Addsimps [length_drop];
@@ -383,7 +383,7 @@
by(nat_ind_tac "n" 1);
by(ALLGOALS Asm_simp_tac);
br allI 1;
-by(res_inst_tac [("xs","xs")]list_cases 1);
+by(exhaust_tac "xs" 1);
by(ALLGOALS Asm_simp_tac);
qed_spec_mp "take_all";
@@ -391,7 +391,7 @@
by(nat_ind_tac "n" 1);
by(ALLGOALS Asm_simp_tac);
br allI 1;
-by(res_inst_tac [("xs","xs")]list_cases 1);
+by(exhaust_tac "xs" 1);
by(ALLGOALS Asm_simp_tac);
qed_spec_mp "drop_all";
@@ -400,7 +400,7 @@
by(nat_ind_tac "n" 1);
by(ALLGOALS Asm_simp_tac);
br allI 1;
-by(res_inst_tac [("xs","xs")]list_cases 1);
+by(exhaust_tac "xs" 1);
by(ALLGOALS Asm_simp_tac);
qed_spec_mp "take_append";
Addsimps [take_append];
@@ -409,7 +409,7 @@
by(nat_ind_tac "n" 1);
by(ALLGOALS Asm_simp_tac);
br allI 1;
-by(res_inst_tac [("xs","xs")]list_cases 1);
+by(exhaust_tac "xs" 1);
by(ALLGOALS Asm_simp_tac);
qed_spec_mp "drop_append";
Addsimps [drop_append];
@@ -418,10 +418,10 @@
by(nat_ind_tac "m" 1);
by(ALLGOALS Asm_simp_tac);
br allI 1;
-by(res_inst_tac [("xs","xs")]list_cases 1);
+by(exhaust_tac "xs" 1);
by(ALLGOALS Asm_simp_tac);
br allI 1;
-by(res_inst_tac [("n","n")]natE 1);
+by(exhaust_tac "n" 1);
by(ALLGOALS Asm_simp_tac);
qed_spec_mp "take_take";
@@ -429,7 +429,7 @@
by(nat_ind_tac "m" 1);
by(ALLGOALS Asm_simp_tac);
br allI 1;
-by(res_inst_tac [("xs","xs")]list_cases 1);
+by(exhaust_tac "xs" 1);
by(ALLGOALS Asm_simp_tac);
qed_spec_mp "drop_drop";
@@ -437,7 +437,7 @@
by(nat_ind_tac "m" 1);
by(ALLGOALS Asm_simp_tac);
br allI 1;
-by(res_inst_tac [("xs","xs")]list_cases 1);
+by(exhaust_tac "xs" 1);
by(ALLGOALS Asm_simp_tac);
qed_spec_mp "take_drop";
@@ -445,7 +445,7 @@
by(nat_ind_tac "n" 1);
by(ALLGOALS Asm_simp_tac);
br allI 1;
-by(res_inst_tac [("xs","xs")]list_cases 1);
+by(exhaust_tac "xs" 1);
by(ALLGOALS Asm_simp_tac);
qed_spec_mp "take_map";
@@ -453,28 +453,26 @@
by(nat_ind_tac "n" 1);
by(ALLGOALS Asm_simp_tac);
br allI 1;
-by(res_inst_tac [("xs","xs")]list_cases 1);
+by(exhaust_tac "xs" 1);
by(ALLGOALS Asm_simp_tac);
qed_spec_mp "drop_map";
-goal thy
- "!n i. i < n --> nth i (take n xs) = nth i xs";
+goal thy "!n i. i < n --> nth i (take n xs) = nth i xs";
by(induct_tac "xs" 1);
by(ALLGOALS Asm_simp_tac);
by(strip_tac 1);
-by(res_inst_tac [("n","n")] natE 1);
+by(exhaust_tac "n" 1);
by(Blast_tac 1);
-by(res_inst_tac [("n","i")] natE 1);
+by(exhaust_tac "i" 1);
by(ALLGOALS (hyp_subst_tac THEN' Asm_full_simp_tac));
qed_spec_mp "nth_take";
Addsimps [nth_take];
-goal thy
- "!xs i. n + i < length xs --> nth i (drop n xs) = nth (n + i) xs";
+goal thy "!xs i. n + i < length xs --> nth i (drop n xs) = nth (n + i) xs";
by(nat_ind_tac "n" 1);
by(ALLGOALS Asm_simp_tac);
br allI 1;
-by(res_inst_tac [("xs","xs")]list_cases 1);
+by(exhaust_tac "xs" 1);
by(ALLGOALS Asm_simp_tac);
qed_spec_mp "nth_drop";
Addsimps [nth_drop];