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 sum_case_empty_empty (also to simpset)
authoroheimb
Fri, 14 Jul 2000 16:28:56 +0200
changeset 9342 d66f25a206b4
parent 9341 40bab6613000
child 9343 1c4754938980
added sum_case_empty_empty (also to simpset)
src/HOL/Map.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Map.ML	Fri Jul 14 16:28:49 2000 +0200
+++ b/src/HOL/Map.ML	Fri Jul 14 16:28:56 2000 +0200
@@ -13,6 +13,12 @@
 qed "empty_def2";
 Addsimps [empty_def2];
 
+Goal "sum_case empty empty = empty";
+by (rtac ext 1);
+by (simp_tac (simpset() addsplits [sum.split]) 1);
+qed "sum_case_empty_empty";
+Addsimps [sum_case_empty_empty];
+
 
 section "map_upd";
isabelle