author | wenzelm |
Sun, 16 Jul 2000 20:50:15 +0200 | |
changeset 9356 | 30c3d3e308ee |
parent 9355 | 1b2cd40579c6 |
child 9357 | f2e806570e83 |
src/HOL/Map.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Map.ML Sun Jul 16 20:49:56 2000 +0200 +++ b/src/HOL/Map.ML Sun Jul 16 20:50:15 2000 +0200 @@ -147,7 +147,7 @@ Goalw [override_def] "f ++ g(x|->y) = (f ++ g)(x|->y)"; by (rtac ext 1); -by (auto_tac (claset_of Map.thy, simpset_of Map.thy)); +by (auto_tac (claset(), simpset())); qed "override_upd"; Addsimps[override_upd];