changeset 3384 | 5ef99c94e1fb |
parent 3356 | 9b899eb8a036 |
child 3415 | c068bd2f0bbd |
--- a/src/HOL/equalities.ML Mon Jun 02 12:13:42 1997 +0200 +++ b/src/HOL/equalities.ML Mon Jun 02 12:14:15 1997 +0200 @@ -228,10 +228,12 @@ goal Set.thy "(insert a B) Un C = insert a (B Un C)"; by (Blast_tac 1); qed "Un_insert_left"; +Addsimps[Un_insert_left]; goal Set.thy "A Un (insert a B) = insert a (A Un B)"; by (Blast_tac 1); qed "Un_insert_right"; +Addsimps[Un_insert_right]; goal Set.thy "(insert a B) Int C = (if a:C then insert a (B Int C) \ \ else B Int C)";