# HG changeset patch
# User haftmann
# Date 1256550701 -3600
# Node ID 247f6c6969d97961f343db62505d7abad5ea78e2
# Parent  de8cc01e8d9e46b7fed2162e2514d91018a2dfa4
tuned code setup for primitive boolean connectors

diff -r de8cc01e8d9e -r 247f6c6969d9 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Oct 26 09:41:26 2009 +0100
+++ b/src/HOL/HOL.thy	Mon Oct 26 10:51:41 2009 +0100
@@ -1827,24 +1827,28 @@
 text {* Code equations *}
 
 lemma [code]:
-  shows "(True \<Longrightarrow> PROP P) \<equiv> PROP P" 
-    and "(False \<Longrightarrow> Q) \<equiv> Trueprop True" 
-    and "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True" 
-    and "(Q \<Longrightarrow> False) \<equiv> Trueprop (\<not> Q)" by (auto intro!: equal_intr_rule)
+  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)
 
 lemma [code]:
-  shows "False \<and> x \<longleftrightarrow> False"
-    and "True \<and> x \<longleftrightarrow> x"
-    and "x \<and> False \<longleftrightarrow> False"
-    and "x \<and> True \<longleftrightarrow> x" by simp_all
+  shows "False \<and> P \<longleftrightarrow> False"
+    and "True \<and> P \<longleftrightarrow> P"
+    and "P \<and> False \<longleftrightarrow> False"
+    and "P \<and> True \<longleftrightarrow> P" by simp_all
 
 lemma [code]:
-  shows "False \<or> x \<longleftrightarrow> x"
-    and "True \<or> x \<longleftrightarrow> True"
-    and "x \<or> False \<longleftrightarrow> x"
-    and "x \<or> True \<longleftrightarrow> True" by simp_all
+  shows "False \<or> P \<longleftrightarrow> P"
+    and "True \<or> P \<longleftrightarrow> True"
+    and "P \<or> False \<longleftrightarrow> P"
+    and "P \<or> True \<longleftrightarrow> True" by simp_all
 
-declare imp_conv_disj [code, code_unfold_post]
+lemma [code]:
+  shows "(False \<longrightarrow> P) \<longleftrightarrow> True"
+    and "(True \<longrightarrow> P) \<longleftrightarrow> P"
+    and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
+    and "(P \<longrightarrow> True) \<longleftrightarrow> True" by simp_all
 
 instantiation itself :: (type) eq
 begin