changeset 61670 | 301e0b4ecd45 |
parent 58927 | cf47382db395 |
child 61890 | f6ded81f5690 |
61669:27ca6147e3b3 | 61670:301e0b4ecd45 |
---|---|
1 theory Collecting_ITP |
1 theory Collecting_ITP |
2 imports "~~/src/Tools/Permanent_Interpretation" Complete_Lattice_ix "ACom_ITP" |
2 imports Complete_Lattice_ix "ACom_ITP" |
3 begin |
3 begin |
4 |
4 |
5 subsection "Collecting Semantics of Commands" |
5 subsection "Collecting Semantics of Commands" |
6 |
6 |
7 subsubsection "Annotated commands as a complete lattice" |
7 subsubsection "Annotated commands as a complete lattice" |