# HG changeset patch
# User paulson
# Date 933162333 -7200
# Node ID 37eccadf6b8a99580d8dae4b7507d7f51ab2d94b
# Parent  8c1caac3e54eb03ba39afef8f7c50b18ddf72cbe
congruence rule for |-

diff -r 8c1caac3e54e -r 37eccadf6b8a src/Sequents/LK.thy
--- 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