# HG changeset patch
# User paulson
# Date 1113903623 -7200
# Node ID 90b6433c6093511af497f5975abb35005a517411
# Parent  38c8ea8521e776306011058ec7f9b0413051247d
fixed presentation

diff -r 38c8ea8521e7 -r 90b6433c6093 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Apr 19 10:59:31 2005 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Apr 19 11:40:23 2005 +0200
@@ -2308,7 +2308,7 @@
 
 text {* Classical rules from the locales are deleted in the above
   interpretations, since they interfere with the claset setup for
-  {text "op \<le>"}. *)
+  @{text "op \<le>"}. *}
 
 text{* Now we instantiate the recursion equations and declare them
 simplification rules: *}