equal
deleted
inserted
replaced
7 relation r over the domain A. |
7 relation r over the domain A. |
8 *) |
8 *) |
9 |
9 |
10 header{*Charpentier's "Increasing" Relation*} |
10 header{*Charpentier's "Increasing" Relation*} |
11 |
11 |
12 theory Increasing = Constrains + Monotonicity: |
12 theory Increasing imports Constrains Monotonicity begin |
13 |
13 |
14 constdefs |
14 constdefs |
15 |
15 |
16 increasing :: "[i, i, i=>i] => i" ("increasing[_]'(_, _')") |
16 increasing :: "[i, i, i=>i] => i" ("increasing[_]'(_, _')") |
17 "increasing[A](r, f) == |
17 "increasing[A](r, f) == |