summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Sequents/LK.thy

author | paulson |

Fri, 05 Oct 2007 09:59:03 +0200 | |

changeset 24854 | 0ebcd575d3c6 |

parent 21428 | f84cf8e9cad8 |

child 27149 | 123377499a8e |

permissions | -rw-r--r-- |

filtering out some package theorems

(* Title: LK/LK.ML 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. 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. *) theory LK imports LK0 uses ("simpdata.ML") begin axioms monotonic: "($H |- P ==> $H |- Q) ==> $H, P |- Q" left_cong: "[| P == P'; |- P' ==> ($H |- $F) == ($H' |- $F') |] ==> (P, $H |- $F) == (P', $H' |- $F')" use "simpdata.ML" end