equal
deleted
inserted
replaced
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 |
12 keywords |
12 keywords |
13 "data_raw" :: thy_decl and |
|
14 "data" :: thy_decl |
13 "data" :: thy_decl |
15 begin |
14 begin |
16 |
15 |
17 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> {}" |
18 by blast |
17 by blast |