src/HOL/Sledgehammer.thy
changeset 37399 34f080a12063
parent 36569 3a29eb7606c3
child 37410 2bf7e6136047
     1.1 --- a/src/HOL/Sledgehammer.thy	Fri Jun 11 17:07:27 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Fri Jun 11 17:10:23 2010 +0200
     1.3 @@ -25,6 +25,12 @@
     1.4    ("Tools/Sledgehammer/metis_tactics.ML")
     1.5  begin
     1.6  
     1.7 +definition skolem_Eps :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" where
     1.8 +[no_atp]: "skolem_Eps = Eps"
     1.9 +
    1.10 +lemma skolem_someI_ex [no_atp]: "\<exists>x. P x \<Longrightarrow> P (skolem_Eps (\<lambda>x. P x))"
    1.11 +unfolding skolem_Eps_def by (rule someI_ex)
    1.12 +
    1.13  definition COMBI :: "'a \<Rightarrow> 'a" where
    1.14  [no_atp]: "COMBI P \<equiv> P"
    1.15