| changeset 48759 | ff570720ba1c |
| parent 48480 | cb03acfae211 |
| child 51625 | bd3358aac5d2 |
| 48749:c197b3c3e7fa | 48759:ff570720ba1c |
|---|---|
3 header "Abstract Interpretation (ITP)" |
3 header "Abstract Interpretation (ITP)" |
4 |
4 |
5 theory Abs_Int0_ITP |
5 theory Abs_Int0_ITP |
6 imports "~~/src/HOL/ex/Interpretation_with_Defs" |
6 imports "~~/src/HOL/ex/Interpretation_with_Defs" |
7 "~~/src/HOL/Library/While_Combinator" |
7 "~~/src/HOL/Library/While_Combinator" |
8 "../Collecting" |
8 "Collecting_ITP" |
9 begin |
9 begin |
10 |
10 |
11 subsection "Orderings" |
11 subsection "Orderings" |
12 |
12 |
13 class preord = |
13 class preord = |