equal
deleted
inserted
replaced
55 |
55 |
56 goal Set.thy "insert x (insert x A) = insert x A"; |
56 goal Set.thy "insert x (insert x A) = insert x A"; |
57 by (Fast_tac 1); |
57 by (Fast_tac 1); |
58 qed "insert_absorb2"; |
58 qed "insert_absorb2"; |
59 Addsimps [insert_absorb2]; |
59 Addsimps [insert_absorb2]; |
|
60 |
|
61 goal Set.thy "insert x (insert y A) = insert y (insert x A)"; |
|
62 by (Fast_tac 1); |
|
63 qed "insert_commute"; |
60 |
64 |
61 goal Set.thy "(insert x A <= B) = (x:B & A <= B)"; |
65 goal Set.thy "(insert x A <= B) = (x:B & A <= B)"; |
62 by (Fast_tac 1); |
66 by (Fast_tac 1); |
63 qed "insert_subset"; |
67 qed "insert_subset"; |
64 Addsimps[insert_subset]; |
68 Addsimps[insert_subset]; |