equal
deleted
inserted
replaced
105 |
105 |
106 |
106 |
107 subsection \<open>Proof theory of propositional logic\<close> |
107 subsection \<open>Proof theory of propositional logic\<close> |
108 |
108 |
109 lemma thms_mono: "G \<subseteq> H \<Longrightarrow> thms(G) \<subseteq> thms(H)" |
109 lemma thms_mono: "G \<subseteq> H \<Longrightarrow> thms(G) \<subseteq> thms(H)" |
110 apply (unfold thms.defs) |
110 unfolding thms.defs |
111 apply (rule lfp_mono) |
111 apply (rule lfp_mono) |
112 apply (rule thms.bnd_mono)+ |
112 apply (rule thms.bnd_mono)+ |
113 apply (assumption | rule univ_mono basic_monos)+ |
113 apply (assumption | rule univ_mono basic_monos)+ |
114 done |
114 done |
115 |
115 |