author | paulson |
Mon, 29 Sep 1997 11:52:25 +0200 | |
changeset 3735 | bed0ba7bff2f |
parent 3734 | 33f355f56f82 |
child 3736 | 39ee3d31cfbc |
--- 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);