src/HOL/HOL.thy

 code_datatype "prop" Trueprop
 
 text {* Code equations *}
 
 lemma [code]:
-  shows "(False \<Longrightarrow> P) \<equiv> Trueprop True" 
-    and "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q" 
-    and "(P \<Longrightarrow> False) \<equiv> Trueprop (\<not> P)"
-    and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True" by (auto intro!: equal_intr_rule)
+  shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q" 
+    and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
+    and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)" by (auto intro!: equal_intr_rule)
 
 lemma [code]:
   shows "False \<and> P \<longleftrightarrow> False"
     and "True \<and> P \<longleftrightarrow> P"
     and "P \<and> False \<longleftrightarrow> False"