src/HOL/Library/List_Prefix.thy
changeset 18258 836491e9b7d5
parent 17201 3bdf1dfcdee4
child 18730 843da46f89ac
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Fri Nov 25 19:09:44 2005 +0100
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Fri Nov 25 19:20:56 2005 +0100
     1.3 @@ -242,12 +242,12 @@
     1.4    by(auto simp add: postfix_def)
     1.5  
     1.6  lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs"
     1.7 -  by (induct zs, auto)
     1.8 +  by (induct zs) auto
     1.9  lemma postfix_is_subset: "xs >>= ys \<Longrightarrow> set ys \<subseteq> set xs"
    1.10    by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma)
    1.11  
    1.12 -lemma postfix_ConsD2_lemma [rule_format]: "x#xs = zs @ y#ys \<longrightarrow> xs >>= ys"
    1.13 -  by (induct zs, auto intro!: postfix_appendI postfix_ConsI)
    1.14 +lemma postfix_ConsD2_lemma: "x#xs = zs @ y#ys \<Longrightarrow> xs >>= ys"
    1.15 +  by (induct zs) (auto intro!: postfix_appendI postfix_ConsI)
    1.16  lemma postfix_ConsD2: "x#xs >>= y#ys \<Longrightarrow> xs >>= ys"
    1.17    by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma)
    1.18