src/HOL/Sledgehammer.thy
changeset 39036 dff91b90d74c
parent 38990 7fba3ccc755a
child 39322 80420a0f2179
     1.1 --- a/src/HOL/Sledgehammer.thy	Thu Sep 02 11:02:13 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Thu Sep 02 11:29:02 2010 +0200
     1.3 @@ -26,6 +26,9 @@
     1.4    ("Tools/Sledgehammer/sledgehammer_isar.ML")
     1.5  begin
     1.6  
     1.7 +lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
     1.8 +by simp
     1.9 +
    1.10  definition skolem_id :: "'a \<Rightarrow> 'a" where
    1.11  [no_atp]: "skolem_id = (\<lambda>x. x)"
    1.12