| changeset 9343 | 1c4754938980 |
| parent 9001 | 93af64f54bf2 |
| child 11655 | 923e4d0d36d5 |
--- a/src/HOL/Option.ML Fri Jul 14 16:28:56 2000 +0200 +++ b/src/HOL/Option.ML Fri Jul 14 16:28:58 2000 +0200 @@ -60,6 +60,13 @@ qed "option_map_eq_Some"; AddIffs[option_map_eq_Some]; +Goal +"option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"; +by (rtac ext 1); +by (simp_tac (simpset() addsplits [sum.split]) 1); +qed "option_map_o_sum_case"; +Addsimps [option_map_o_sum_case]; + section "o2s";