equal
deleted
inserted
replaced
11 |
11 |
12 theory BNF_LFP |
12 theory BNF_LFP |
13 imports BNF_FP_Base |
13 imports BNF_FP_Base |
14 keywords |
14 keywords |
15 "datatype_new" :: thy_decl and |
15 "datatype_new" :: thy_decl and |
16 "datatype_compat" :: thy_decl |
16 "datatype_compat" :: thy_decl and |
|
17 "primrec" :: thy_decl |
17 begin |
18 begin |
18 |
19 |
19 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}" |
20 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}" |
20 by blast |
21 by blast |
21 |
22 |