src/HOL/HOL.thy
changeset 62958 b41c1cb5e251
parent 62913 13252110a6fe
child 63561 fba08009ff3e
     1.1 --- a/src/HOL/HOL.thy	Tue Apr 12 13:49:37 2016 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Apr 12 14:38:57 2016 +0200
     1.3 @@ -747,7 +747,7 @@
     1.4  lemma swap: "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"
     1.5    by (rule classical) iprover
     1.6  
     1.7 -lemma thin_refl: "\<And>X. \<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W" .
     1.8 +lemma thin_refl: "\<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W" .
     1.9  
    1.10  ML \<open>
    1.11  structure Hypsubst = Hypsubst
    1.12 @@ -1506,7 +1506,7 @@
    1.13    unfolding induct_true_def
    1.14    by (iprover intro: equal_intr_rule)
    1.15  
    1.16 -lemma [induct_simp]: "(\<And>x. induct_true) \<equiv> Trueprop induct_true"
    1.17 +lemma [induct_simp]: "(\<And>x::'a::{}. induct_true) \<equiv> Trueprop induct_true"
    1.18    unfolding induct_true_def
    1.19    by (iprover intro: equal_intr_rule)
    1.20