equal
deleted
inserted
replaced
13 imports BNF_Fixpoint_Base |
13 imports BNF_Fixpoint_Base |
14 keywords |
14 keywords |
15 "datatype_new" :: thy_decl and |
15 "datatype_new" :: thy_decl and |
16 "datatype_compat" :: thy_decl |
16 "datatype_compat" :: thy_decl |
17 begin |
17 begin |
18 |
|
19 ML {* proofs := 2 *} (*###*) |
|
20 ML {* Proofterm.proofs_enabled () *} |
|
21 |
18 |
22 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}" |
19 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}" |
23 by blast |
20 by blast |
24 |
21 |
25 lemma image_Collect_subsetI: "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B" |
22 lemma image_Collect_subsetI: "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B" |