equal
deleted
inserted
replaced
326 Goalw [localTo_def, stable_def, constrains_def] |
326 Goalw [localTo_def, stable_def, constrains_def] |
327 "v localTo F <= (f o v) localTo F"; |
327 "v localTo F <= (f o v) localTo F"; |
328 by (Clarify_tac 1); |
328 by (Clarify_tac 1); |
329 by (force_tac (claset() addSEs [allE, ballE], simpset()) 1); |
329 by (force_tac (claset() addSEs [allE, ballE], simpset()) 1); |
330 qed "localTo_imp_o_localTo"; |
330 qed "localTo_imp_o_localTo"; |
|
331 |
|
332 Goalw [localTo_def, stable_def, constrains_def] |
|
333 "(%s. x) localTo F = UNIV"; |
|
334 by (Blast_tac 1); |
|
335 qed "triv_localTo_eq_UNIV"; |
331 |
336 |
332 Goal "(F Join G : v localTo H) = (F : v localTo H & G : v localTo H)"; |
337 Goal "(F Join G : v localTo H) = (F : v localTo H & G : v localTo H)"; |
333 by (asm_full_simp_tac |
338 by (asm_full_simp_tac |
334 (simpset() addsimps [localTo_def, Diff_Join_distrib, |
339 (simpset() addsimps [localTo_def, Diff_Join_distrib, |
335 stable_def, Join_constrains]) 1); |
340 stable_def, Join_constrains]) 1); |