--- 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)
--- 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"
--- 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)