equal
deleted
inserted
replaced
52 by (Asm_simp_tac 1); |
52 by (Asm_simp_tac 1); |
53 qed "assign_different"; |
53 qed "assign_different"; |
54 |
54 |
55 goalw thy [assign_def] "s[s x/x] = s"; |
55 goalw thy [assign_def] "s[s x/x] = s"; |
56 by (rtac ext 1); |
56 by (rtac ext 1); |
57 by (simp_tac (simpset() addsplits [expand_if]) 1); |
57 by (Simp_tac 1); |
58 qed "assign_triv"; |
58 qed "assign_triv"; |
59 |
59 |
60 Addsimps [assign_same, assign_different, assign_triv]; |
60 Addsimps [assign_same, assign_different, assign_triv]; |