tuned;
authorwenzelm
Sat Nov 04 18:41:37 2000 +0100 (2000-11-04)
changeset 10392f27afee8475d
parent 10391 0025fd11882c
child 10393 b2a212304fb4
tuned;
src/HOL/Library/Multiset.thy
src/HOL/Library/Quotient.thy
src/HOL/Library/While_Combinator_Example.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Sat Nov 04 18:39:44 2000 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Sat Nov 04 18:41:37 2000 +0100
     1.3 @@ -443,7 +443,7 @@
     1.4        (\<forall>b. b :# K --> (b, a) \<in> r)}"
     1.5  
     1.6    mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set"
     1.7 -  "mult r == (mult1 r)^+"
     1.8 +  "mult r == (mult1 r)\<^sup>+"
     1.9  
    1.10  lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
    1.11    by (simp add: mult1_def)
     2.1 --- a/src/HOL/Library/Quotient.thy	Sat Nov 04 18:39:44 2000 +0100
     2.2 +++ b/src/HOL/Library/Quotient.thy	Sat Nov 04 18:41:37 2000 +0100
     2.3 @@ -36,7 +36,7 @@
     2.4   \emph{equivalence classes} over elements of the base type @{typ 'a}.
     2.5  *}
     2.6  
     2.7 -typedef 'a quot = "{{x. a \<sim> x}| a::'a::eqv. True}"
     2.8 +typedef 'a quot = "{{x. a \<sim> x} | a::'a::eqv. True}"
     2.9    by blast
    2.10  
    2.11  lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
     3.1 --- a/src/HOL/Library/While_Combinator_Example.thy	Sat Nov 04 18:39:44 2000 +0100
     3.2 +++ b/src/HOL/Library/While_Combinator_Example.thy	Sat Nov 04 18:41:37 2000 +0100
     3.3 @@ -7,11 +7,11 @@
     3.4   An example of using the @{term while} combinator.
     3.5  *}
     3.6  
     3.7 -lemma aux: "{f n| n. A n \<or> B n} = {f n| n. A n} \<union> {f n| n. B n}"
     3.8 +lemma aux: "{f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
     3.9    apply blast
    3.10    done
    3.11  
    3.12 -theorem "P (lfp (\<lambda>N::int set. {#0} \<union> {(n + #2) mod #6| n. n \<in> N})) =
    3.13 +theorem "P (lfp (\<lambda>N::int set. {#0} \<union> {(n + #2) mod #6 | n. n \<in> N})) =
    3.14      P {#0, #4, #2}"
    3.15    apply (subst lfp_conv_while [where ?U = "{#0, #1, #2, #3, #4, #5}"])
    3.16       apply (rule monoI)