author | haftmann |
Mon, 28 Nov 2005 13:43:56 +0100 | |
changeset 18278 | cbf6f44d73d3 |
parent 18019 | d1ff9ebb8bcb |
child 18466 | 389a6f9c31f4 |
permissions | -rw-r--r-- |
(* Title: Pure/Pure.thy ID: $Id$ The Pure theory. *) theory Pure imports ProtoPure begin setup "Context.setup ()" text{* These meta-level elimination rules facilitate the use of assumptions that contain !! and ==>, especially in linear scripts. *} lemma meta_mp: assumes "PROP P ==> PROP Q" and "PROP P" shows "PROP Q" by (rule `PROP P ==> PROP Q` [OF `PROP P`]) lemma meta_spec: assumes "!!x. PROP P(x)" shows "PROP P(x)" by (rule `!!x. PROP P(x)`) lemmas meta_allE = meta_spec [elim_format] end