fixed presentation
authorpaulson
Tue, 19 Apr 2005 11:40:23 +0200
changeset 15770 90b6433c6093
parent 15769 38c8ea8521e7
child 15771 08cc20626a0f
fixed presentation
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: *}