| changeset 51390 | 1dff81cf425b |
| parent 51389 | 8a9f0503b1c0 |
| child 53013 | 3fbcfa911863 |
| 51389:8a9f0503b1c0 | 51390:1dff81cf425b |
|---|---|
1 theory Abs_Int_init |
1 theory Abs_Int_init |
2 imports "~~/src/HOL/Library/While_Combinator" |
2 imports "~~/src/HOL/Library/While_Combinator" |
3 "~~/src/HOL/Library/Quotient_List" |
|
4 "~~/src/HOL/Library/Extended" |
|
3 Vars Collecting Abs_Int_Tests |
5 Vars Collecting Abs_Int_Tests |
4 begin |
6 begin |
5 |
7 |
6 hide_const (open) top bot dom --"to avoid qualified names" |
8 hide_const (open) top bot dom --"to avoid qualified names" |
7 |
9 |
8 end |
10 end |