# HG changeset patch
# User haftmann
# Date 1263224702 -3600
# Node ID c6449a41b214311b6ca4144dcbf28104ce87836b
# Parent  6ca970cfa873e9ef2665fcdbb4ec651e5cf35ea0
tuned code equations

diff -r 6ca970cfa873 -r c6449a41b214 src/HOL/HOL.thy
--- 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"