changeset 47613 | e72e44cee6f2 |
parent 47602 | 3d44790b5ab0 |
child 47818 | 151d137f1095 |
47603:b716b16ab2ac | 47613:e72e44cee6f2 |
---|---|
1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
2 |
|
3 header "Abstract Interpretation (ITP)" |
|
2 |
4 |
3 theory Abs_Int0_ITP |
5 theory Abs_Int0_ITP |
4 imports "~~/src/HOL/ex/Interpretation_with_Defs" |
6 imports "~~/src/HOL/ex/Interpretation_with_Defs" |
5 "~~/src/HOL/Library/While_Combinator" |
7 "~~/src/HOL/Library/While_Combinator" |
6 Collecting |
8 Collecting |