equal
deleted
inserted
replaced
11 qed "getlocs_def2"; |
11 qed "getlocs_def2"; |
12 |
12 |
13 Goalw [update_def] "s[Loc Y::=s<Y>] = s"; |
13 Goalw [update_def] "s[Loc Y::=s<Y>] = s"; |
14 by (induct_tac "s" 1); |
14 by (induct_tac "s" 1); |
15 by (simp_tac (simpset() addsimps [getlocs_def2]) 1); |
15 by (simp_tac (simpset() addsimps [getlocs_def2]) 1); |
16 br ext 1; |
|
17 by (Simp_tac 1); |
|
18 qed "update_Loc_idem2"; |
16 qed "update_Loc_idem2"; |
19 Addsimps[update_Loc_idem2]; |
17 Addsimps[update_Loc_idem2]; |
20 |
18 |
21 Goalw [update_def] "s[X::=x][X::=y] = s[X::=y]"; |
19 Goalw [update_def] "s[X::=x][X::=y] = s[X::=y]"; |
22 by (induct_tac "X" 1); |
20 by (induct_tac "X" 1); |