equal
deleted
inserted
replaced
4 |
4 |
5 Increasing's parameters are a state function f, a domain A and an order |
5 Increasing's parameters are a state function f, a domain A and an order |
6 relation r over the domain A. |
6 relation r over the domain A. |
7 *) |
7 *) |
8 |
8 |
9 section{*Charpentier's "Increasing" Relation*} |
9 section\<open>Charpentier's "Increasing" Relation\<close> |
10 |
10 |
11 theory Increasing imports Constrains Monotonicity begin |
11 theory Increasing imports Constrains Monotonicity begin |
12 |
12 |
13 definition |
13 definition |
14 increasing :: "[i, i, i=>i] => i" ("increasing[_]'(_, _')") where |
14 increasing :: "[i, i, i=>i] => i" ("increasing[_]'(_, _')") where |