src/HOL/Sledgehammer.thy
changeset 39355 104a6d9e493e
parent 39322 80420a0f2179
child 39452 70a57e40f795
     1.1 --- a/src/HOL/Sledgehammer.thy	Tue Sep 14 08:50:46 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Tue Sep 14 09:12:28 2010 +0200
     1.3 @@ -29,8 +29,8 @@
     1.4  lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
     1.5  by simp
     1.6  
     1.7 -definition skolem_id :: "'a \<Rightarrow> 'a" where
     1.8 -[no_atp]: "skolem_id = (\<lambda>x. x)"
     1.9 +definition skolem :: "'a \<Rightarrow> 'a" where
    1.10 +[no_atp]: "skolem = (\<lambda>x. x)"
    1.11  
    1.12  definition COMBI :: "'a \<Rightarrow> 'a" where
    1.13  [no_atp]: "COMBI P = P"