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