equal
deleted
inserted
replaced
8 *) |
8 *) |
9 |
9 |
10 header {* Shared Fixed Point Operations on Bounded Natural Functors *} |
10 header {* Shared Fixed Point Operations on Bounded Natural Functors *} |
11 |
11 |
12 theory BNF_FP_Base |
12 theory BNF_FP_Base |
13 imports BNF_Comp |
13 imports BNF_Comp Basic_BNFs |
14 begin |
14 begin |
15 |
15 |
16 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q" |
16 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q" |
17 by auto |
17 by auto |
18 |
18 |