| changeset 51389 | 8a9f0503b1c0 |
| parent 47613 | e72e44cee6f2 |
| child 51390 | 1dff81cf425b |
--- a/src/HOL/IMP/Abs_Int_init.thy Sun Mar 10 14:36:18 2013 +0100 +++ b/src/HOL/IMP/Abs_Int_init.thy Sun Mar 10 18:29:10 2013 +0100 @@ -1,6 +1,5 @@ theory Abs_Int_init -imports "~~/src/HOL/ex/Interpretation_with_Defs" - "~~/src/HOL/Library/While_Combinator" +imports "~~/src/HOL/Library/While_Combinator" Vars Collecting Abs_Int_Tests begin