equal
deleted
inserted
replaced
31 Goalw [update_def] "domain(f(x:=y)) = cons(x, domain(f))"; |
31 Goalw [update_def] "domain(f(x:=y)) = cons(x, domain(f))"; |
32 by (Asm_simp_tac 1); |
32 by (Asm_simp_tac 1); |
33 qed "domain_update"; |
33 qed "domain_update"; |
34 Addsimps [domain_update]; |
34 Addsimps [domain_update]; |
35 |
35 |
|
36 Goalw [update_def] "[| f: A -> B; x : A; y: B |] ==> f(x:=y) : A -> B"; |
|
37 by (asm_simp_tac (simpset() addsimps [domain_of_fun, cons_absorb, |
|
38 apply_funtype, lam_type]) 1); |
|
39 qed "update_type"; |
|
40 |
|
41 |