# HG changeset patch
# User wenzelm
# Date 973359697 -3600
# Node ID f27afee8475da9fe944cd2e9ebe5e5ab5b7e4464
# Parent  0025fd11882ca6694596ad6145547f6b13b981f3
tuned;

diff -r 0025fd11882c -r f27afee8475d src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Nov 04 18:39:44 2000 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Nov 04 18:41:37 2000 +0100
@@ -443,7 +443,7 @@
       (\<forall>b. b :# K --> (b, a) \<in> r)}"
 
   mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set"
-  "mult r == (mult1 r)^+"
+  "mult r == (mult1 r)\<^sup>+"
 
 lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
   by (simp add: mult1_def)
diff -r 0025fd11882c -r f27afee8475d src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Sat Nov 04 18:39:44 2000 +0100
+++ b/src/HOL/Library/Quotient.thy	Sat Nov 04 18:41:37 2000 +0100
@@ -36,7 +36,7 @@
  \emph{equivalence classes} over elements of the base type @{typ 'a}.
 *}
 
-typedef 'a quot = "{{x. a \<sim> x}| a::'a::eqv. True}"
+typedef 'a quot = "{{x. a \<sim> x} | a::'a::eqv. True}"
   by blast
 
 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
diff -r 0025fd11882c -r f27afee8475d src/HOL/Library/While_Combinator_Example.thy
--- a/src/HOL/Library/While_Combinator_Example.thy	Sat Nov 04 18:39:44 2000 +0100
+++ b/src/HOL/Library/While_Combinator_Example.thy	Sat Nov 04 18:41:37 2000 +0100
@@ -7,11 +7,11 @@
  An example of using the @{term while} combinator.
 *}
 
-lemma aux: "{f n| n. A n \<or> B n} = {f n| n. A n} \<union> {f n| n. B n}"
+lemma aux: "{f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
   apply blast
   done
 
-theorem "P (lfp (\<lambda>N::int set. {#0} \<union> {(n + #2) mod #6| n. n \<in> N})) =
+theorem "P (lfp (\<lambda>N::int set. {#0} \<union> {(n + #2) mod #6 | n. n \<in> N})) =
     P {#0, #4, #2}"
   apply (subst lfp_conv_while [where ?U = "{#0, #1, #2, #3, #4, #5}"])
      apply (rule monoI)