| changeset 8600 | a466c687c726 |
| parent 8177 | e59e93ad85eb |
| child 10962 | cda180b1e2e0 |
--- a/src/HOL/IMPP/Misc.ML Tue Mar 28 12:28:24 2000 +0200 +++ b/src/HOL/IMPP/Misc.ML Tue Mar 28 17:31:36 2000 +0200 @@ -13,8 +13,6 @@ Goalw [update_def] "s[Loc Y::=s<Y>] = s"; by (induct_tac "s" 1); by (simp_tac (simpset() addsimps [getlocs_def2]) 1); -br ext 1; -by (Simp_tac 1); qed "update_Loc_idem2"; Addsimps[update_Loc_idem2];