equal
deleted
inserted
replaced
14 Swiss Federal Institute of Technology Zurich (1997) |
14 Swiss Federal Institute of Technology Zurich (1997) |
15 *) |
15 *) |
16 |
16 |
17 header{*Progress Sets*} |
17 header{*Progress Sets*} |
18 |
18 |
19 theory ProgressSets = Transformers: |
19 theory ProgressSets imports Transformers begin |
20 |
20 |
21 subsection {*Complete Lattices and the Operator @{term cl}*} |
21 subsection {*Complete Lattices and the Operator @{term cl}*} |
22 |
22 |
23 constdefs |
23 constdefs |
24 lattice :: "'a set set => bool" |
24 lattice :: "'a set set => bool" |