changeset 48480 | cb03acfae211 |
parent 47818 | 151d137f1095 |
child 52046 | bc01725d7918 |
48479:819f7a5f3e7f | 48480:cb03acfae211 |
---|---|
1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
2 |
2 |
3 header "Denotational Abstract Interpretation" |
3 header "Denotational Abstract Interpretation" |
4 |
4 |
5 theory Abs_Int_den0_fun |
5 theory Abs_Int_den0_fun |
6 imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step |
6 imports "~~/src/HOL/ex/Interpretation_with_Defs" "../Big_Step" |
7 begin |
7 begin |
8 |
8 |
9 subsection "Orderings" |
9 subsection "Orderings" |
10 |
10 |
11 class preord = |
11 class preord = |