| changeset 15770 | 90b6433c6093 |
| parent 15765 | 6472d4942992 |
| child 15780 | 6744bba5561d |
--- 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: *}