1.1 --- a/src/HOL/Finite_Set.thy	Tue Apr 19 10:59:31 2005 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Apr 19 11:40:23 2005 +0200
     1.3 @@ -2308,7 +2308,7 @@
     1.4  
     1.5  text {* Classical rules from the locales are deleted in the above
     1.6    interpretations, since they interfere with the claset setup for
     1.7 -  {text "op \<le>"}. *)
     1.8 +  @{text "op \<le>"}. *}
     1.9  
    1.10  text{* Now we instantiate the recursion equations and declare them
    1.11  simplification rules: *}