author wenzelm
Sat, 23 Apr 2005 19:49:39 +0200
changeset 15824 222eeb9655f3
parent 15803 42c75e0c9140
child 18019 d1ff9ebb8bcb
permissions -rw-r--r--
tuned proofs;

(*  Title:      Pure/Pure.thy
    ID:         $Id$
    Author:     Larry Paulson and Makarius

The Pure theory.

theory Pure
imports ProtoPure

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 major: "PROP P ==> PROP Q" and minor: "PROP P"
  shows "PROP Q"
    by (rule major [OF minor])

lemma meta_spec:
  assumes major: "!!x. PROP P(x)"
  shows "PROP P(x)"
    by (rule major)

lemmas meta_allE = meta_spec [elim_format]