changeset 15650 | b37dc98fbbc5 |
parent 15576 | efb95d0d01f7 |
child 15651 | 4b393520846e |
15649:f8345ee4f607 | 15650:b37dc98fbbc5 |
---|---|
3 Author: Franz Regensburger |
3 Author: Franz Regensburger |
4 |
4 |
5 Top theory for HOLCF system. |
5 Top theory for HOLCF system. |
6 *) |
6 *) |
7 |
7 |
8 HOLCF = Sprod + Ssum + Up + Lift + Discrete + One + Tr |
8 theory HOLCF |
9 imports Sprod Ssum Up Lift Discrete One Tr |
|
10 begin |
|
11 |
|
12 end |