# HG changeset patch
# User wenzelm
# Date 1331737179 -3600
# Node ID aa862ff8a8a926648d17551de6caf90c9a5ceb5b
# Parent  5f44c8bea84effd8a3099cce90fc549d720bc401
some proof indentation;

diff -r 5f44c8bea84e -r aa862ff8a8a9 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Mar 14 15:37:51 2012 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Mar 14 15:59:39 2012 +0100
@@ -118,8 +118,8 @@
 lemma count_union [simp]: "count (M + N) a = count M a + count N a"
   by (simp add: union_def in_multiset multiset_typedef)
 
-instance multiset :: (type) cancel_comm_monoid_add proof
-qed (simp_all add: multiset_eq_iff)
+instance multiset :: (type) cancel_comm_monoid_add
+  by default (simp_all add: multiset_eq_iff)
 
 
 subsubsection {* Difference *}
@@ -270,8 +270,8 @@
 definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
   mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
 
-instance proof
-qed (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym)
+instance
+  by default (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym)
 
 end
 
@@ -377,10 +377,11 @@
 definition inf_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
   multiset_inter_def: "inf_multiset A B = A - (A - B)"
 
-instance proof -
+instance
+proof -
   have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" by arith
-  show "OFCLASS('a multiset, semilattice_inf_class)" proof
-  qed (auto simp add: multiset_inter_def mset_le_def aux)
+  show "OFCLASS('a multiset, semilattice_inf_class)"
+    by default (auto simp add: multiset_inter_def mset_le_def aux)
 qed
 
 end
@@ -822,7 +823,8 @@
 lemma multiset_of_eq_length:
   assumes "multiset_of xs = multiset_of ys"
   shows "length xs = length ys"
-using assms proof (induct xs arbitrary: ys)
+using assms
+proof (induct xs arbitrary: ys)
   case Nil then show ?case by simp
 next
   case (Cons x xs)
@@ -845,7 +847,8 @@
 next
   case True
   moreover have "z \<in># multiset_of ys" using assms True by simp
-  show ?thesis using assms proof (induct xs arbitrary: ys)
+  show ?thesis using assms
+  proof (induct xs arbitrary: ys)
     case Nil then show ?case by simp
   next
     case (Cons x xs)
@@ -864,7 +867,8 @@
   assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
     and equiv: "multiset_of xs = multiset_of ys"
   shows "fold f xs = fold f ys"
-using f equiv [symmetric] proof (induct xs arbitrary: ys)
+using f equiv [symmetric]
+proof (induct xs arbitrary: ys)
   case Nil then show ?case by simp
 next
   case (Cons x xs)
@@ -898,7 +902,8 @@
   and "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>x. f k = f x) ys = filter (\<lambda>x. f k = f x) xs"
   and "sorted (map f ys)"
   shows "sort_key f xs = ys"
-using assms proof (induct xs arbitrary: ys)
+using assms
+proof (induct xs arbitrary: ys)
   case Nil then show ?case by simp
 next
   case (Cons x xs)
@@ -994,10 +999,12 @@
 proof (cases xs)
   case Nil then show ?thesis by simp
 next
-  case (Cons _ ys) note hyps = Cons show ?thesis proof (cases ys)
+  case (Cons _ ys) note hyps = Cons show ?thesis
+  proof (cases ys)
     case Nil with hyps show ?thesis by simp
   next
-    case (Cons _ zs) note hyps = hyps Cons show ?thesis proof (cases zs)
+    case (Cons _ zs) note hyps = hyps Cons show ?thesis
+    proof (cases zs)
       case Nil with hyps show ?thesis by auto
     next
       case Cons 
@@ -1224,8 +1231,8 @@
 definition
   [code]: "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
 
-instance proof
-qed (simp add: equal_multiset_def eq_iff)
+instance
+  by default (simp add: equal_multiset_def eq_iff)
 
 end
 
@@ -1512,8 +1519,8 @@
   qed
   have trans: "\<And>K M N :: 'a multiset. K \<subset># M \<Longrightarrow> M \<subset># N \<Longrightarrow> K \<subset># N"
     unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
-  show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
-  qed (auto simp add: le_multiset_def irrefl dest: trans)
+  show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset"
+    by default (auto simp add: le_multiset_def irrefl dest: trans)
 qed
 
 lemma mult_less_irrefl [elim!]: "M \<subset># (M::'a::order multiset) ==> R"
@@ -1785,14 +1792,12 @@
 
 enriched_type image_mset: image_mset
 proof -
-  fix f g 
-  show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
+  fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
   proof
     fix A
     show "(image_mset f \<circ> image_mset g) A = image_mset (f \<circ> g) A"
       by (induct A) simp_all
   qed
-next
   show "image_mset id = id"
   proof
     fix A