Commit c0e4dfe9 authored by Miriam's avatar Miriam

changed comment about the disjunction, box free and shallow remains

parent ff26261e
......@@ -494,7 +494,8 @@ Qed.
(** ** Lemma 4 from the corrected ALCOP slides *)
(** Following are concrete examples of envelopes. We first tried to prove adequateness without envelopes, but it turned out our restrictions were stronger than necessary. Still they are relevant for practical purpose and we will now show that our results apply to them as well.
(** Following are concrete examples of envelopes. Our first attempt at proving adequateness was done with axioms being either disjunction free ([dis_free_under_box]) and [shallow] or completely [box_free].
It turned out that we could prove adequateness for an even less restrictive class of logics using envelopes. Still those stronger requirements are relevant for practical purpose and we will now show that our results apply to them as well.
*)
Lemma sub_vars_dneg_eq:
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment