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.
merged
authorblanchet
Tue, 14 Sep 2010 08:50:46 +0200
changeset 39354 cd20519eb9d0
parent 39314 aecb239a2bbc (diff)
parent 39353 7f11d833d65b (current diff)
child 39355 104a6d9e493e
merged
src/Tools/Metis/src/PP.sig file | annotate | diff | comparison | revisions
src/Tools/Metis/src/PP.sml file | annotate | diff | comparison | revisions
src/Tools/Metis/src/Parser.sig file | annotate | diff | comparison | revisions
src/Tools/Metis/src/Parser.sml file | annotate | diff | comparison | revisions
src/Tools/Metis/src/PortableIsabelle.sml file | annotate | diff | comparison | revisions
src/Tools/Metis/src/RandomMap.sml file | annotate | diff | comparison | revisions
src/Tools/Metis/src/RandomSet.sml file | annotate | diff | comparison | revisions
src/Tools/auto_counterexample.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Multiset.thy	Mon Sep 13 21:24:10 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue Sep 14 08:50:46 2010 +0200
@@ -1381,14 +1381,6 @@
 
 lemma fold_mset_insert:
   "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)"
-apply (simp add: fold_mset_def fold_mset_insert_aux add_commute)  
-apply (rule the_equality)
- apply (auto cong add: conj_cong 
-     simp add: fold_mset_def [symmetric] fold_mset_equality fold_msetG_nonempty)
-done
-
-lemma fold_mset_insert_idem:
-  "fold_mset f z (A + {#a#}) = f a (fold_mset f z A)"
 apply (simp add: fold_mset_def fold_mset_insert_aux)
 apply (rule the_equality)
  apply (auto cong add: conj_cong
isabelle