src/Pure/Pure.thy
author wenzelm
Sat Apr 23 19:49:39 2005 +0200 (2005-04-23)
changeset 15824 222eeb9655f3
parent 15803 42c75e0c9140
child 18019 d1ff9ebb8bcb
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      Pure/Pure.thy
     2     ID:         $Id$
     3     Author:     Larry Paulson and Makarius
     4 
     5 The Pure theory.
     6 *)
     7 
     8 theory Pure
     9 imports ProtoPure
    10 begin
    11 
    12 setup "Context.setup ()"
    13 
    14 
    15 text{*These meta-level elimination rules facilitate the use of assumptions
    16 that contain !! and ==>, especially in linear scripts. *}
    17 
    18 lemma meta_mp:
    19   assumes major: "PROP P ==> PROP Q" and minor: "PROP P"
    20   shows "PROP Q"
    21     by (rule major [OF minor])
    22 
    23 lemma meta_spec:
    24   assumes major: "!!x. PROP P(x)"
    25   shows "PROP P(x)"
    26     by (rule major)
    27 
    28 lemmas meta_allE = meta_spec [elim_format]
    29 
    30 end