equal
deleted
inserted
replaced
219 qed "domI"; |
219 qed "domI"; |
220 |
220 |
221 Goalw [dom_def] "a : dom m ==> ? b. m a = Some b"; |
221 Goalw [dom_def] "a : dom m ==> ? b. m a = Some b"; |
222 by Auto_tac; |
222 by Auto_tac; |
223 qed "domD"; |
223 qed "domD"; |
224 AddSDs [domD]; |
224 |
|
225 Goalw [dom_def] "(a : dom m) = (m a ~= None)"; |
|
226 by Auto_tac; |
|
227 qed "domIff"; |
|
228 AddIffs [domIff]; |
|
229 Delsimps [domIff]; |
225 |
230 |
226 Goalw [dom_def] "dom empty = {}"; |
231 Goalw [dom_def] "dom empty = {}"; |
227 by (Simp_tac 1); |
232 by (Simp_tac 1); |
228 qed "dom_empty"; |
233 qed "dom_empty"; |
229 Addsimps [dom_empty]; |
234 Addsimps [dom_empty]; |