src/Pure/Pure.thy
changeset 26958 ed3a58a9eae1
parent 26572 9178a7f4c4c8
child 27681 8cedebf55539
     1.1 --- a/src/Pure/Pure.thy	Sun May 18 17:03:20 2008 +0200
     1.2 +++ b/src/Pure/Pure.thy	Sun May 18 17:03:23 2008 +0200
     1.3 @@ -14,14 +14,14 @@
     1.4  lemmas meta_impE = meta_mp [elim_format]
     1.5  
     1.6  lemma meta_spec:
     1.7 -  assumes "!!x. PROP P(x)"
     1.8 -  shows "PROP P(x)"
     1.9 -    by (rule `!!x. PROP P(x)`)
    1.10 +  assumes "!!x. PROP P x"
    1.11 +  shows "PROP P x"
    1.12 +    by (rule `!!x. PROP P x`)
    1.13  
    1.14  lemmas meta_allE = meta_spec [elim_format]
    1.15  
    1.16  lemma swap_params:
    1.17 -  "(!!x y. PROP P(x, y)) == (!!y x. PROP P(x, y))" ..
    1.18 +  "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
    1.19  
    1.20  
    1.21  subsection {* Embedded terms *}
    1.22 @@ -39,22 +39,22 @@
    1.23  
    1.24  lemma all_conjunction:
    1.25    includes meta_conjunction_syntax
    1.26 -  shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
    1.27 +  shows "(!!x. PROP A x && PROP B x) == ((!!x. PROP A x) && (!!x. PROP B x))"
    1.28  proof
    1.29 -  assume conj: "!!x. PROP A(x) && PROP B(x)"
    1.30 -  show "(!!x. PROP A(x)) && (!!x. PROP B(x))"
    1.31 +  assume conj: "!!x. PROP A x && PROP B x"
    1.32 +  show "(!!x. PROP A x) && (!!x. PROP B x)"
    1.33    proof -
    1.34      fix x
    1.35 -    from conj show "PROP A(x)" by (rule conjunctionD1)
    1.36 -    from conj show "PROP B(x)" by (rule conjunctionD2)
    1.37 +    from conj show "PROP A x" by (rule conjunctionD1)
    1.38 +    from conj show "PROP B x" by (rule conjunctionD2)
    1.39    qed
    1.40  next
    1.41 -  assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
    1.42 +  assume conj: "(!!x. PROP A x) && (!!x. PROP B x)"
    1.43    fix x
    1.44 -  show "PROP A(x) && PROP B(x)"
    1.45 +  show "PROP A x && PROP B x"
    1.46    proof -
    1.47 -    show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
    1.48 -    show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
    1.49 +    show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
    1.50 +    show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
    1.51    qed
    1.52  qed
    1.53