author | oheimb |
Mon, 27 Apr 1998 19:29:19 +0200 | |
changeset 4836 | fc5773ae2790 |
parent 4835 | f90a427d903f |
child 4837 | eab729051897 |
src/HOL/Option.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Option.ML Mon Apr 27 18:06:22 1998 +0200 +++ b/src/HOL/Option.ML Mon Apr 27 19:29:19 1998 +0200 @@ -56,8 +56,7 @@ val option_map_eq_Some = prove_goalw thy [option_map_def] "(option_map f xo = Some y) = (? z. xo = Some z & f z = y)" (K [asm_full_simp_tac (simpset() addsplits [split_option_case]) 1]); -AddSDs[option_map_eq_Some RS iffD1]; -Addsimps [option_map_eq_Some]; +AddIffs[option_map_eq_Some]; section "o2s";