src/Pure/Pure.thy
author obua
Sun May 29 12:39:12 2005 +0200 (2005-05-29)
changeset 16108 cf468b93a02e
parent 15824 222eeb9655f3
child 18019 d1ff9ebb8bcb
permissions -rw-r--r--
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
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@15824
    21
    by (rule major [OF minor])
wenzelm@15803
    22
wenzelm@15803
    23
lemma meta_spec:
wenzelm@15803
    24
  assumes major: "!!x. PROP P(x)"
wenzelm@15803
    25
  shows "PROP P(x)"
wenzelm@15824
    26
    by (rule major)
wenzelm@15803
    27
wenzelm@15803
    28
lemmas meta_allE = meta_spec [elim_format]
wenzelm@15803
    29
wenzelm@15803
    30
end