src/HOL/Sledgehammer.thy
changeset 37410 2bf7e6136047
parent 37399 34f080a12063
child 37509 f39464d971c4
     1.1 --- a/src/HOL/Sledgehammer.thy	Sat Jun 12 15:48:17 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Mon Jun 14 10:36:01 2010 +0200
     1.3 @@ -25,11 +25,8 @@
     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 +definition skolem_id :: "'a \<Rightarrow> 'a" where
    1.13 +[no_atp]: "skolem_id = (\<lambda>x. x)"
    1.14  
    1.15  definition COMBI :: "'a \<Rightarrow> 'a" where
    1.16  [no_atp]: "COMBI P \<equiv> P"