equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 header {* Library for Bounded Natural Functors *} |
9 header {* Library for Bounded Natural Functors *} |
10 |
10 |
11 theory BNF_Util |
11 theory BNF_Util |
12 imports "../Cardinals/Cardinal_Arithmetic" |
12 imports Ctr_Sugar "../Cardinals/Cardinal_Arithmetic" |
13 begin |
13 begin |
14 |
14 |
15 lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)" |
15 lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)" |
16 by blast |
16 by blast |
17 |
17 |