tuned proofs;
authorwenzelm
Sat Apr 23 19:49:39 2005 +0200 (2005-04-23 ago)
changeset 15824222eeb9655f3
parent 15823 d1001770af17
child 15825 1576f9d3ffae
tuned proofs;
src/Pure/Pure.thy
     1.1 --- a/src/Pure/Pure.thy	Sat Apr 23 19:49:26 2005 +0200
     1.2 +++ b/src/Pure/Pure.thy	Sat Apr 23 19:49:39 2005 +0200
     1.3 @@ -18,16 +18,12 @@
     1.4  lemma meta_mp:
     1.5    assumes major: "PROP P ==> PROP Q" and minor: "PROP P"
     1.6    shows "PROP Q"
     1.7 -proof -
     1.8 -  show "PROP Q" by (rule major [OF minor])
     1.9 -qed
    1.10 +    by (rule major [OF minor])
    1.11  
    1.12  lemma meta_spec:
    1.13    assumes major: "!!x. PROP P(x)"
    1.14    shows "PROP P(x)"
    1.15 -proof -
    1.16 -  show "PROP P(x)" by (rule major)
    1.17 -qed
    1.18 +    by (rule major)
    1.19  
    1.20  lemmas meta_allE = meta_spec [elim_format]
    1.21