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