equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header {* Least Fixed Point Operation on Bounded Natural Functors *} |
8 header {* Least Fixed Point Operation on Bounded Natural Functors *} |
9 |
9 |
10 theory BNF_LFP |
10 theory BNF_LFP |
11 imports BNF_FP |
11 imports BNF_FP_Basic |
12 keywords |
12 keywords |
13 "datatype_new" :: thy_decl |
13 "datatype_new" :: thy_decl |
14 begin |
14 begin |
15 |
15 |
16 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}" |
16 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}" |