src/HOL/Library/BigO.thy
changeset 61585 a9599d3d7610
parent 60500 903bb1495239
child 61762 d50b993b4fb9
     1.1 --- a/src/HOL/Library/BigO.thy	Thu Nov 05 10:35:37 2015 +0100
     1.2 +++ b/src/HOL/Library/BigO.thy	Thu Nov 05 10:39:49 2015 +0100
     1.3 @@ -16,20 +16,20 @@
     1.4  
     1.5  The main changes in this version are as follows:
     1.6  \begin{itemize}
     1.7 -\item We have eliminated the @{text O} operator on sets. (Most uses of this seem
     1.8 +\item We have eliminated the \<open>O\<close> operator on sets. (Most uses of this seem
     1.9    to be inessential.)
    1.10 -\item We no longer use @{text "+"} as output syntax for @{text "+o"}
    1.11 -\item Lemmas involving @{text "sumr"} have been replaced by more general lemmas
    1.12 -  involving `@{text "setsum"}.
    1.13 +\item We no longer use \<open>+\<close> as output syntax for \<open>+o\<close>
    1.14 +\item Lemmas involving \<open>sumr\<close> have been replaced by more general lemmas
    1.15 +  involving `\<open>setsum\<close>.
    1.16  \item The library has been expanded, with e.g.~support for expressions of
    1.17 -  the form @{text "f < g + O(h)"}.
    1.18 +  the form \<open>f < g + O(h)\<close>.
    1.19  \end{itemize}
    1.20  
    1.21  Note also since the Big O library includes rules that demonstrate set
    1.22  inclusion, to use the automated reasoners effectively with the library
    1.23 -one should redeclare the theorem @{text "subsetI"} as an intro rule,
    1.24 -rather than as an @{text "intro!"} rule, for example, using
    1.25 -\isa{\isakeyword{declare}}~@{text "subsetI [del, intro]"}.
    1.26 +one should redeclare the theorem \<open>subsetI\<close> as an intro rule,
    1.27 +rather than as an \<open>intro!\<close> rule, for example, using
    1.28 +\isa{\isakeyword{declare}}~\<open>subsetI [del, intro]\<close>.
    1.29  \<close>
    1.30  
    1.31  subsection \<open>Definitions\<close>