changeset 51390 | 1dff81cf425b |
parent 51389 | 8a9f0503b1c0 |
child 53013 | 3fbcfa911863 |
--- a/src/HOL/IMP/Abs_Int_init.thy Sun Mar 10 18:29:10 2013 +0100 +++ b/src/HOL/IMP/Abs_Int_init.thy Mon Mar 11 12:27:31 2013 +0100 @@ -1,8 +1,10 @@ theory Abs_Int_init imports "~~/src/HOL/Library/While_Combinator" + "~~/src/HOL/Library/Quotient_List" + "~~/src/HOL/Library/Extended" Vars Collecting Abs_Int_Tests begin -hide_const (open) top bot dom --"to avoid qualified names" +hide_const (open) top bot dom --"to avoid qualified names" end