# HG changeset patch
# User obua
# Date 1084136676 -7200
# Node ID 8e739a6eaf1124d5845625d5a651b59f78703b12
# Parent  782932b1e931c2f6774f94131d6806a138254fef
replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style

diff -r 782932b1e931 -r 8e739a6eaf11 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun May 09 16:39:29 2004 +0200
+++ b/src/HOL/Library/Multiset.thy	Sun May 09 23:04:36 2004 +0200
@@ -109,11 +109,12 @@
 theorems union_ac = union_assoc union_commute union_lcomm
 
 instance multiset :: (type) plus_ac0
-  apply intro_classes
-    apply (rule union_commute)
-   apply (rule union_assoc)
-  apply simp
-  done
+proof 
+  fix a b c :: "'a multiset"
+  show "(a + b) + c = a + (b + c)" by (rule union_assoc)
+  show "a + b = b + a" by (rule union_commute)
+  show "0 + a = a" by simp
+qed
 
 
 subsubsection {* Difference *}