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)