| changeset 63680 | 6e1e8b5abbfa |
| parent 63485 | ea8dfb0ed10e |
| child 64267 | b9a1486e79be |
--- a/src/HOL/Library/Set_Algebras.thy Fri Aug 12 17:49:02 2016 +0200 +++ b/src/HOL/Library/Set_Algebras.thy Fri Aug 12 17:53:55 2016 +0200 @@ -13,7 +13,7 @@ text \<open> This library lifts operations like addition and multiplication to sets. It was designed to support asymptotic calculations. See the comments at the top - of @{file "BigO.thy"}. + of \<^file>\<open>BigO.thy\<close>. \<close> instantiation set :: (plus) plus