tuned whitespace
authorhaftmann
Mon Feb 20 21:04:00 2012 +0100 (2012-02-20)
changeset 465562848e36e0348
parent 46555 c2b5900988e2
child 46557 ae926869a311
tuned whitespace
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Product_Type.thy	Mon Feb 20 08:01:08 2012 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Mon Feb 20 21:04:00 2012 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4  lemma
     1.5    shows [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
     1.6      and [code]: "HOL.equal True P \<longleftrightarrow> P" 
     1.7 -    and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P" 
     1.8 +    and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P"
     1.9      and [code]: "HOL.equal P True \<longleftrightarrow> P"
    1.10      and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
    1.11    by (simp_all add: equal)