# HG changeset patch
# User nipkow
# Date 962890680 -7200
# Node ID 4313b08b6e1b53c95bf6a888864423f4ee7a7f9a
# Parent  dbf30a2d1b565947cb4bb36943feae0da3f4adb7
Deleted list_case thms no subsumed by case_tac

diff -r dbf30a2d1b56 -r 4313b08b6e1b src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Jul 06 15:36:59 2000 +0200
+++ b/src/HOL/List.ML	Thu Jul 06 15:38:00 2000 +0200
@@ -48,21 +48,11 @@
 qed "lists_Int_eq";
 Addsimps [lists_Int_eq];
 
-
-(**  Case analysis **)
-section "Case analysis";
-
-val prems = Goal "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
-by (induct_tac "xs" 1);
-by (REPEAT(resolve_tac prems 1));
-qed "list_cases";
-
-Goal "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
-by (induct_tac "xs" 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
-bind_thm("list_eq_cases",
-  impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
+Goal "(xs@ys : lists A) = (xs : lists A & ys : lists A)";
+by(induct_tac "xs" 1);
+by(Auto_tac);
+qed "append_in_lists_conv";
+AddIffs [append_in_lists_conv];
 
 (** length **)
 (* needs to come before "@" because of thm append_eq_append_conv *)