src/HOL/List.ML
changeset 4032 4b1c69d8b767
parent 3919 c036caebfc75
child 4069 d6d06a03a2e9
     1.1 --- a/src/HOL/List.ML	Wed Oct 29 16:03:19 1997 +0100
     1.2 +++ b/src/HOL/List.ML	Thu Oct 30 09:45:03 1997 +0100
     1.3 @@ -48,13 +48,7 @@
     1.4  
     1.5  (** list_case **)
     1.6  
     1.7 -goal thy
     1.8 - "P(list_case a f xs) = ((xs=[] --> P(a)) & \
     1.9 -\                        (!y ys. xs=y#ys --> P(f y ys)))";
    1.10 -by (induct_tac "xs" 1);
    1.11 -by (ALLGOALS Asm_simp_tac);
    1.12 -by (Blast_tac 1);
    1.13 -qed "expand_list_case";
    1.14 +val expand_list_case = split_list_case;
    1.15  
    1.16  val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
    1.17  by (induct_tac "xs" 1);