equal
deleted
inserted
replaced
10 header {* Least Fixed Point Operation on Bounded Natural Functors *} |
10 header {* Least Fixed Point Operation on Bounded Natural Functors *} |
11 |
11 |
12 theory BNF_Least_Fixpoint |
12 theory BNF_Least_Fixpoint |
13 imports BNF_Fixpoint_Base |
13 imports BNF_Fixpoint_Base |
14 keywords |
14 keywords |
15 "datatype" :: thy_decl and |
|
16 "datatype" :: thy_decl and |
15 "datatype" :: thy_decl and |
17 "datatype_compat" :: thy_decl |
16 "datatype_compat" :: thy_decl |
18 begin |
17 begin |
19 |
18 |
20 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> {}" |