src/HOL/List.thy
changeset 46884 154dc6ec0041
parent 46698 f1dfcf8be88d
child 46898 1570b30ee040
     1.1 --- a/src/HOL/List.thy	Mon Mar 12 15:12:22 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Mon Mar 12 21:41:11 2012 +0100
     1.3 @@ -4533,7 +4533,7 @@
     1.4    "listsp A (x # xs)"
     1.5  
     1.6  lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
     1.7 -by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)
     1.8 +by (rule predicate1I, erule listsp.induct, blast+)
     1.9  
    1.10  lemmas lists_mono = listsp_mono [to_set]
    1.11