src/Pure/Pure.thy
changeset 18019 d1ff9ebb8bcb
parent 15824 222eeb9655f3
child 18466 389a6f9c31f4
     1.1 --- a/src/Pure/Pure.thy	Fri Oct 28 20:18:37 2005 +0200
     1.2 +++ b/src/Pure/Pure.thy	Fri Oct 28 22:26:10 2005 +0200
     1.3 @@ -1,6 +1,5 @@
     1.4  (*  Title:      Pure/Pure.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Larry Paulson and Makarius
     1.7  
     1.8  The Pure theory.
     1.9  *)
    1.10 @@ -12,18 +11,18 @@
    1.11  setup "Context.setup ()"
    1.12  
    1.13  
    1.14 -text{*These meta-level elimination rules facilitate the use of assumptions
    1.15 -that contain !! and ==>, especially in linear scripts. *}
    1.16 +text{* These meta-level elimination rules facilitate the use of assumptions
    1.17 +  that contain !! and ==>, especially in linear scripts. *}
    1.18  
    1.19  lemma meta_mp:
    1.20 -  assumes major: "PROP P ==> PROP Q" and minor: "PROP P"
    1.21 +  assumes "PROP P ==> PROP Q" and "PROP P"
    1.22    shows "PROP Q"
    1.23 -    by (rule major [OF minor])
    1.24 +    by (rule `PROP P ==> PROP Q` [OF `PROP P`])
    1.25  
    1.26  lemma meta_spec:
    1.27 -  assumes major: "!!x. PROP P(x)"
    1.28 +  assumes "!!x. PROP P(x)"
    1.29    shows "PROP P(x)"
    1.30 -    by (rule major)
    1.31 +    by (rule `!!x. PROP P(x)`)
    1.32  
    1.33  lemmas meta_allE = meta_spec [elim_format]
    1.34