src/HOL/Library/FuncSet.thy
changeset 44382 9afa4a0e6f3c
parent 40631 b3f85ba3dae4
child 47761 dfe747e72fa8
     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