Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added option_map_o_sum_case (also to simpset)
authoroheimb
Fri, 14 Jul 2000 16:28:58 +0200
changeset 9343 1c4754938980
parent 9342 d66f25a206b4
child 9344 6c85c8bdd2ed
added option_map_o_sum_case (also to simpset)
src/HOL/Option.ML file | annotate | diff | comparison | revisions 
--- 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";
isabelle