| changeset 7499 | 23e090051cb8 |
| parent 6068 | 2d8f3e1f1151 |
| child 9683 | f87c8c449018 |
--- a/src/ZF/Coind/Map.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/Coind/Map.ML Tue Sep 07 10:40:58 1999 +0200 @@ -134,7 +134,7 @@ Goalw [PMap_def] "[| m:PMap(A,B); a:domain(m) |] ==> map_app(m,a):B"; -by (forward_tac [tmap_app_notempty] 1); +by (ftac tmap_app_notempty 1); by (assume_tac 1); by (dtac tmap_appI 1); by (assume_tac 1);