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;
wenzelm@15803
     1
(*  Title:      Pure/Pure.thy
wenzelm@15803
     2
    ID:         $Id$
wenzelm@15803
     3
wenzelm@15803
     4
The Pure theory.
wenzelm@15803
     5
*)
wenzelm@15803
     6
wenzelm@15803
     7
theory Pure
wenzelm@15803
     8
imports ProtoPure
wenzelm@15803
     9
begin
wenzelm@15803
    10
wenzelm@15803
    11
setup "Context.setup ()"
wenzelm@15803
    12
wenzelm@15803
    13
wenzelm@18019
    14
text{* These meta-level elimination rules facilitate the use of assumptions
wenzelm@18019
    15
  that contain !! and ==>, especially in linear scripts. *}
wenzelm@15803
    16
wenzelm@15803
    17
lemma meta_mp:
wenzelm@18019
    18
  assumes "PROP P ==> PROP Q" and "PROP P"
wenzelm@15803
    19
  shows "PROP Q"
wenzelm@18019
    20
    by (rule `PROP P ==> PROP Q` [OF `PROP P`])
wenzelm@15803
    21
wenzelm@15803
    22
lemma meta_spec:
wenzelm@18019
    23
  assumes "!!x. PROP P(x)"
wenzelm@15803
    24
  shows "PROP P(x)"
wenzelm@18019
    25
    by (rule `!!x. PROP P(x)`)
wenzelm@15803
    26
wenzelm@15803
    27
lemmas meta_allE = meta_spec [elim_format]
wenzelm@15803
    28
wenzelm@15803
    29
end