equal
deleted
inserted
replaced
76 (** map_owr **) |
76 (** map_owr **) |
77 |
77 |
78 |
78 |
79 goalw Map.thy [map_owr_def,PMap_def,TMap_def] |
79 goalw Map.thy [map_owr_def,PMap_def,TMap_def] |
80 "!! A.[| m:PMap(A,B); a:A; b:B |] ==> map_owr(m,a,b):PMap(A,B)"; |
80 "!! A.[| m:PMap(A,B); a:A; b:B |] ==> map_owr(m,a,b):PMap(A,B)"; |
81 by (Step_tac 1); |
81 by Safe_tac; |
82 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [if_iff]))); |
82 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [if_iff]))); |
83 by (Fast_tac 1); |
83 by (Fast_tac 1); |
84 by (Fast_tac 1); |
84 by (Fast_tac 1); |
85 by (Deepen_tac 2 1); |
85 by (Deepen_tac 2 1); |
86 (*Remaining subgoal*) |
86 (*Remaining subgoal*) |