| changeset 8423 | 3c19160b6432 |
| parent 8327 | 108fcc85a767 |
| child 8442 | 96023903c2df |
--- a/src/HOL/UNITY/Lift_prog.ML Mon Mar 13 12:42:41 2000 +0100 +++ b/src/HOL/UNITY/Lift_prog.ML Mon Mar 13 12:51:10 2000 +0100 @@ -16,7 +16,7 @@ Goal "(insert_map i x (delete_map i g)) = g(i:=x)"; by (rtac ext 1); by (auto_tac (claset(), simpset() addsplits [nat_diff_split])); -by (exhaust_tac "d" 1); +by (cases_tac "d" 1); by (ALLGOALS Asm_simp_tac); qed "insert_map_delete_map_eq";