src/HOL/SMT.thy
changeset 40806 59d96f777da3
parent 40681 872b08416fb4
child 41059 d2b1fc1b8e19
     1.1 --- a/src/HOL/SMT.thy	Mon Nov 29 11:39:00 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Mon Nov 29 23:41:09 2010 +0100
     1.3 @@ -324,6 +324,7 @@
     1.4    "(if P then True else False) = P"
     1.5    "(if P then False else True) = (\<not>P)"
     1.6    "(if \<not>P then x else y) = (if P then y else x)"
     1.7 +  "f (if P then x else y) = (if P then f x else f y)"
     1.8    by auto
     1.9  
    1.10  lemma [z3_rule]: