src/HOL/Sledgehammer.thy

--- a/src/HOL/Sledgehammer.thy	Thu Sep 02 11:02:13 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Thu Sep 02 11:29:02 2010 +0200
@@ -26,6 +26,9 @@
   ("Tools/Sledgehammer/sledgehammer_isar.ML")
 begin
 
+lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
+by simp
+
 definition skolem_id :: "'a \<Rightarrow> 'a" where
 [no_atp]: "skolem_id = (\<lambda>x. x)"