# HG changeset patch
# User nipkow
# Date 864286777 -7200
# Node ID 0db086394024caf7fa954b4576063733e1e03cc9
# Parent  c31e6239d4c93938c12810529f1c14fce82d0b83
Replaced res_inst-list_cases by generic exhaust_tac.

diff -r c31e6239d4c9 -r 0db086394024 src/HOL/List.ML
--- 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];