src/HOL/SMT.thy

--- a/src/HOL/SMT.thy	Mon Nov 29 11:39:00 2010 +0100
+++ b/src/HOL/SMT.thy	Mon Nov 29 23:41:09 2010 +0100
@@ -324,6 +324,7 @@
   "(if P then True else False) = P"
   "(if P then False else True) = (\<not>P)"
   "(if \<not>P then x else y) = (if P then y else x)"
+  "f (if P then x else y) = (if P then f x else f y)"
   by auto
 
 lemma [z3_rule]: