src/HOL/SMT.thy
changeset 45392 828e08541cee
parent 44488 587bf61a00a1
child 46950 d0181abdbdac
     1.1 --- a/src/HOL/SMT.thy	Mon Nov 07 17:24:57 2011 +0100
     1.2 +++ b/src/HOL/SMT.thy	Mon Nov 07 17:54:35 2011 +0100
     1.3 @@ -393,7 +393,6 @@
     1.4    "(if P then x = y else x = z) = (x = (if P then y else z))"
     1.5    "(if P then x = y else y = z) = (y = (if P then x else z))"
     1.6    "(if P then x = y else z = y) = (y = (if P then x else z))"
     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]: