changeset 51389 | 8a9f0503b1c0 |
parent 47613 | e72e44cee6f2 |
child 51390 | 1dff81cf425b |
51388:1f5497c8ce8c | 51389:8a9f0503b1c0 |
---|---|
1 theory Abs_Int_init |
1 theory Abs_Int_init |
2 imports "~~/src/HOL/ex/Interpretation_with_Defs" |
2 imports "~~/src/HOL/Library/While_Combinator" |
3 "~~/src/HOL/Library/While_Combinator" |
|
4 Vars Collecting Abs_Int_Tests |
3 Vars Collecting Abs_Int_Tests |
5 begin |
4 begin |
6 |
5 |
7 hide_const (open) top bot dom --"to avoid qualified names" |
6 hide_const (open) top bot dom --"to avoid qualified names" |
8 |
7 |