| changeset 36452 | d37c6eed8117 |
| parent 35901 | 12f09bf2c77f |
| child 39971 | 2949af5e6b9c |
| 36451:ddc965e172c4 | 36452:d37c6eed8117 |
|---|---|
6 |
6 |
7 theory Deflation |
7 theory Deflation |
8 imports Cfun |
8 imports Cfun |
9 begin |
9 begin |
10 |
10 |
11 defaultsort cpo |
11 default_sort cpo |
12 |
12 |
13 subsection {* Continuous deflations *} |
13 subsection {* Continuous deflations *} |
14 |
14 |
15 locale deflation = |
15 locale deflation = |
16 fixes d :: "'a \<rightarrow> 'a" |
16 fixes d :: "'a \<rightarrow> 'a" |