Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/BigO.thy
changeset 80914 d97fdabd9e2b
parent 79566 f783490c6c99 
--- a/src/HOL/ex/BigO.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/ex/BigO.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -35,7 +35,7 @@
 
 subsection \<open>Definitions\<close>
 
-definition bigo :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(1O'(_'))")
+definition bigo :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) set"  (\<open>(1O'(_'))\<close>)
   where "O(f:: 'a \<Rightarrow> 'b) = {h. \<exists>c. \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>}"
 
 lemma bigo_pos_const:
@@ -407,7 +407,7 @@
 
 subsection \<open>Less than or equal to\<close>
 
-definition lesso :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"  (infixl "<o" 70)
+definition lesso :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"  (infixl \<open><o\<close> 70)
   where "f <o g = (\<lambda>x. max (f x - g x) 0)"
 
 lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. \<bar>g x\<bar> \<le> \<bar>f x\<bar> \<Longrightarrow> g =o O(h)"
isabelle