| changeset 18413 | 50c0c118e96d |
| parent 16417 | 9bc16273c2d4 |
| child 19736 | d8d0f8f51d69 |
--- a/src/HOL/Induct/Sexp.thy Thu Dec 15 18:13:40 2005 +0100 +++ b/src/HOL/Induct/Sexp.thy Thu Dec 15 19:42:00 2005 +0100 @@ -65,9 +65,7 @@ by blast lemma Scons_D: "Scons M N \<in> sexp ==> M \<in> sexp & N \<in> sexp" -apply (erule setup_induction) -apply (erule sexp.induct, blast+) -done + by (induct S == "Scons M N" set: sexp) auto (** Introduction rules for 'pred_sexp' **)