tuned;
authorwenzelm
Fri Oct 28 22:26:10 2005 +0200 (2005-10-28)
changeset 18019d1ff9ebb8bcb
parent 18018 82206a6c75c0
child 18020 d23a846598d2
tuned;
src/Pure/CPure.thy
src/Pure/Pure.thy
     1.1 --- a/src/Pure/CPure.thy	Fri Oct 28 20:18:37 2005 +0200
     1.2 +++ b/src/Pure/CPure.thy	Fri Oct 28 22:26:10 2005 +0200
     1.3 @@ -1,6 +1,5 @@
     1.4  (*  Title:      Pure/CPure.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Makarius
     1.7  
     1.8  The CPure theory -- Pure with alternative application syntax.
     1.9  *)
     2.1 --- a/src/Pure/Pure.thy	Fri Oct 28 20:18:37 2005 +0200
     2.2 +++ b/src/Pure/Pure.thy	Fri Oct 28 22:26:10 2005 +0200
     2.3 @@ -1,6 +1,5 @@
     2.4  (*  Title:      Pure/Pure.thy
     2.5      ID:         $Id$
     2.6 -    Author:     Larry Paulson and Makarius
     2.7  
     2.8  The Pure theory.
     2.9  *)
    2.10 @@ -12,18 +11,18 @@
    2.11  setup "Context.setup ()"
    2.12  
    2.13  
    2.14 -text{*These meta-level elimination rules facilitate the use of assumptions
    2.15 -that contain !! and ==>, especially in linear scripts. *}
    2.16 +text{* These meta-level elimination rules facilitate the use of assumptions
    2.17 +  that contain !! and ==>, especially in linear scripts. *}
    2.18  
    2.19  lemma meta_mp:
    2.20 -  assumes major: "PROP P ==> PROP Q" and minor: "PROP P"
    2.21 +  assumes "PROP P ==> PROP Q" and "PROP P"
    2.22    shows "PROP Q"
    2.23 -    by (rule major [OF minor])
    2.24 +    by (rule `PROP P ==> PROP Q` [OF `PROP P`])
    2.25  
    2.26  lemma meta_spec:
    2.27 -  assumes major: "!!x. PROP P(x)"
    2.28 +  assumes "!!x. PROP P(x)"
    2.29    shows "PROP P(x)"
    2.30 -    by (rule major)
    2.31 +    by (rule `!!x. PROP P(x)`)
    2.32  
    2.33  lemmas meta_allE = meta_spec [elim_format]
    2.34