| changeset 2034 | 5079fdf938dd |
| parent 1461 | 6bcb44e4d6e5 |
| child 2469 | b50b8c0eec01 |
--- a/src/ZF/Coind/Values.ML Thu Sep 26 15:14:23 1996 +0200 +++ b/src/ZF/Coind/Values.ML Thu Sep 26 15:49:54 1996 +0200 @@ -89,7 +89,7 @@ by (cut_facts_tac prems 1); by (etac ValEnvE 1); by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1); -by (rtac (map_domain_owr RS ssubst) 1); +by (stac map_domain_owr 1); by (assume_tac 1); by (rtac Un_commute 1); qed "ve_dom_owr";