--- a/src/Sequents/LK.thy Wed Jul 28 13:42:20 1999 +0200
+++ b/src/Sequents/LK.thy Wed Jul 28 13:45:33 1999 +0200
@@ -6,6 +6,9 @@
Axiom to express monotonicity (a variant of the deduction theorem). Makes the
link between |- and ==>, needed for instance to prove imp_cong.
+Axiom left_cong allows the simplifier to use left-side formulas. Ideally it
+should be derived from lower-level axioms.
+
CANNOT be added to LK0.thy because modal logic is built upon it, and
various modal rules would become inconsistent.
*)
@@ -16,4 +19,6 @@
monotonic "($H |- P ==> $H |- Q) ==> $H, P |- Q"
+ left_cong "[| P == P'; |- P' ==> ($H |- $F) == ($H' |- $F') |]
+ ==> (P, $H |- $F) == (P', $H' |- $F')"
end