equal
deleted
inserted
replaced
10 section \<open>Least Fixpoint (Datatype) Operation on Bounded Natural Functors\<close> |
10 section \<open>Least Fixpoint (Datatype) Operation on Bounded Natural Functors\<close> |
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 |
15 "datatype" :: thy_defn and |
16 "datatype_compat" :: thy_decl |
16 "datatype_compat" :: thy_defn |
17 begin |
17 begin |
18 |
18 |
19 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> {}" |
20 by blast |
20 by blast |
21 |
21 |