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