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