reduced warnings;
authorwenzelm
Mon Aug 22 20:11:44 2011 +0200 (2011-08-22)
changeset 443829afa4a0e6f3c
parent 44381 c38bb61deeaa
child 44383 f99906c2a1d3
reduced warnings;
src/HOL/Library/FuncSet.thy
     1.1 --- a/src/HOL/Library/FuncSet.thy	Mon Aug 22 20:00:04 2011 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Mon Aug 22 20:11:44 2011 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4    by (auto simp: Pi_def)
     1.5  
     1.6  lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A"
     1.7 -  by (auto intro: Pi_I)
     1.8 +  by auto
     1.9  
    1.10  lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B"
    1.11    by (simp add: Pi_def)
    1.12 @@ -257,7 +257,7 @@
    1.13  where "extensional_funcset S T = (S -> T) \<inter> (extensional S)"
    1.14  
    1.15  lemma extensional_empty[simp]: "extensional {} = {%x. undefined}"
    1.16 -unfolding extensional_def by (auto intro: ext)
    1.17 +unfolding extensional_def by auto
    1.18  
    1.19  lemma extensional_funcset_empty_domain: "extensional_funcset {} T = {%x. undefined}"
    1.20  unfolding extensional_funcset_def by simp