changeset 67443 | 3abf6a722518 |
parent 67406 | 23307fd33906 |
67442:f075640b8868 | 67443:3abf6a722518 |
---|---|
2 imports "HOL-Library.While_Combinator" |
2 imports "HOL-Library.While_Combinator" |
3 "HOL-Library.Extended" |
3 "HOL-Library.Extended" |
4 Vars Collecting Abs_Int_Tests |
4 Vars Collecting Abs_Int_Tests |
5 begin |
5 begin |
6 |
6 |
7 hide_const (open) top bot dom \<comment>"to avoid qualified names" |
7 hide_const (open) top bot dom \<comment> \<open>to avoid qualified names\<close> |
8 |
8 |
9 end |
9 end |