equal
deleted
inserted
replaced
12 "~~/src/HOL/Decision_Procs/Dense_Linear_Order" |
12 "~~/src/HOL/Decision_Procs/Dense_Linear_Order" |
13 Main |
13 Main |
14 "~~/src/HOL/Library/Function_Algebras" |
14 "~~/src/HOL/Library/Function_Algebras" |
15 "~~/src/HOL/Library/Set_Algebras" |
15 "~~/src/HOL/Library/Set_Algebras" |
16 begin |
16 begin |
|
17 |
|
18 declare [[metis_new_skolemizer]] |
17 |
19 |
18 subsection {* Definitions *} |
20 subsection {* Definitions *} |
19 |
21 |
20 definition bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set" ("(1O'(_'))") where |
22 definition bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set" ("(1O'(_'))") where |
21 "O(f::('a => 'b)) == {h. EX c. ALL x. abs (h x) <= c * abs (f x)}" |
23 "O(f::('a => 'b)) == {h. EX c. ALL x. abs (h x) <= c * abs (f x)}" |