author paulson
Tue, 27 Jul 1999 18:52:48 +0200
changeset 7094 6f18ae72a90e
parent 6456 23602e214ebf
child 7117 37eccadf6b8a
permissions -rw-r--r--
a new theory containing just an axiom needed to derive imp_cong

(*  Title:      LK/LK
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Axiom to express monotonicity (a variant of the deduction theorem).  Makes the
link between |- and ==>, needed for instance to prove imp_cong.

CANNOT be added to LK0.thy because modal logic is built upon it, and
various modal rules would become inconsistent.

LK = LK0 +


  monotonic  "($H |- P ==> $H |- Q) ==> $H, P |- Q"