changeset 61585 | a9599d3d7610 |
parent 61337 | 4645502c3c64 |
child 63473 | 151bb79536a7 |
--- a/src/HOL/Library/Set_Algebras.thy Thu Nov 05 10:35:37 2015 +0100 +++ b/src/HOL/Library/Set_Algebras.thy Thu Nov 05 10:39:49 2015 +0100 @@ -11,7 +11,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 theory @{text BigO}. + comments at the top of theory \<open>BigO\<close>. \<close> instantiation set :: (plus) plus