--- a/src/HOL/HOL.thy Tue Jun 06 19:24:05 2006 +0200
+++ b/src/HOL/HOL.thy Tue Jun 06 20:42:25 2006 +0200
@@ -1124,11 +1124,11 @@
by (simplesubst split_if, blast)
lemma if_bool_eq_conj: "(if P then Q else R) = ((P-->Q) & (~P-->R))"
- -- {* This form is useful for expanding @{text if}s on the RIGHT of the @{text "==>"} symbol. *}
+ -- {* This form is useful for expanding @{text "if"}s on the RIGHT of the @{text "==>"} symbol. *}
by (rule split_if)
lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))"
- -- {* And this form is useful for expanding @{text if}s on the LEFT. *}
+ -- {* And this form is useful for expanding @{text "if"}s on the LEFT. *}
apply (simplesubst split_if, blast)
done