changeset 18413 | 50c0c118e96d |
parent 16417 | 9bc16273c2d4 |
child 19736 | d8d0f8f51d69 |
--- a/src/HOL/Induct/SList.thy Thu Dec 15 18:13:40 2005 +0100 +++ b/src/HOL/Induct/SList.thy Thu Dec 15 19:42:00 2005 +0100 @@ -295,9 +295,7 @@ lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE, standard] lemma CONS_D: "CONS M N: list(A) ==> M: A & N: list(A)" -apply (erule setup_induction) -apply (erule list.induct, blast+) -done + by (induct L == "CONS M N" set: list) auto lemma sexp_CONS_D: "CONS M N: sexp ==> M: sexp & N: sexp" apply (simp add: CONS_def In1_def)