changeset 3735 | bed0ba7bff2f |
parent 2493 | bdeb5024353a |
child 3840 | e0baea4d485a |
--- a/src/ZF/Coind/Map.ML Mon Sep 29 11:51:52 1997 +0200 +++ b/src/ZF/Coind/Map.ML Mon Sep 29 11:52:25 1997 +0200 @@ -78,7 +78,7 @@ goalw Map.thy [map_owr_def,PMap_def,TMap_def] "!! A.[| m:PMap(A,B); a:A; b:B |] ==> map_owr(m,a,b):PMap(A,B)"; -by (Step_tac 1); +by Safe_tac; by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [if_iff]))); by (Fast_tac 1); by (Fast_tac 1);