--- a/src/HOL/HOL.thy Mon Jan 11 11:47:38 2010 +0100
+++ b/src/HOL/HOL.thy Mon Jan 11 16:45:02 2010 +0100
@@ -1816,10 +1816,9 @@
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"