fix/fixes: tuned type constraints;
authorwenzelm
Sat Jun 24 22:54:37 2006 +0200 (2006-06-24)
changeset 199490505dce27b0b
parent 19948 1be283f3f1ba
child 19950 fd74bf4e603e
fix/fixes: tuned type constraints;
src/HOL/Library/Ramsey.thy
     1.1 --- a/src/HOL/Library/Ramsey.thy	Sat Jun 24 22:25:31 2006 +0200
     1.2 +++ b/src/HOL/Library/Ramsey.thy	Sat Jun 24 22:54:37 2006 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4      by (auto intro: someI2_ex)
     1.5    show "\<forall>n m. n<m --> (choice P r n, choice P r m) \<in> r"
     1.6    proof (intro strip)
     1.7 -    fix n and m::nat
     1.8 +    fix n m :: nat
     1.9      assume less: "n<m"
    1.10      show "(choice P r n, choice P r m) \<in> r" using PSuc
    1.11        by (auto intro: less_Suc_induct [OF less] transD [OF trans])
    1.12 @@ -73,7 +73,7 @@
    1.13  subsection {*Ramsey's Theorem: Infinitary Version*}
    1.14  
    1.15  lemma ramsey_induction: 
    1.16 -  fixes s::nat and r::nat
    1.17 +  fixes s r :: nat
    1.18    shows
    1.19    "!!(YY::'a set) (f::'a set => nat). 
    1.20        [|infinite YY; part r s YY f|]
    1.21 @@ -147,7 +147,7 @@
    1.22      with pg [of n'] have less': "s'<s" by (cases "g n'") auto
    1.23      have inj_gy: "inj ?gy"
    1.24      proof (rule linorder_injI)
    1.25 -      fix m and m'::nat assume less: "m < m'" show "?gy m \<noteq> ?gy m'"
    1.26 +      fix m m' :: nat assume less: "m < m'" show "?gy m \<noteq> ?gy m'"
    1.27          using rg [OF less] pg [of m] by (cases "g m", cases "g m'") auto
    1.28      qed
    1.29      show ?thesis
    1.30 @@ -205,7 +205,7 @@
    1.31  
    1.32  text{*Repackaging of Tom Ridge's final result*}
    1.33  theorem Ramsey:
    1.34 -  fixes s::nat and r::nat and Z::"'a set" and f::"'a set => nat"
    1.35 +  fixes s r :: nat and Z::"'a set" and f::"'a set => nat"
    1.36    shows
    1.37     "[|infinite Z;
    1.38        \<forall>X. X \<subseteq> Z & finite X & card X = r --> f X < s|]