author | paulson |
Tue, 27 Jul 1999 18:52:48 +0200 | |
changeset 7094 | 6f18ae72a90e |
parent 6456 | 23602e214ebf |
child 7117 | 37eccadf6b8a |
permissions | -rw-r--r-- |
(* 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 + rules monotonic "($H |- P ==> $H |- Q) ==> $H, P |- Q" end