changeset 48480 | cb03acfae211 |
parent 47818 | 151d137f1095 |
child 51698 | c0af8bbc5825 |
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Tue Jul 24 17:33:19 2012 +0200 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Tue Jul 24 17:34:46 2012 +0200 @@ -1,7 +1,7 @@ (* Author: Tobias Nipkow *) theory Abs_Int2_ITP -imports Abs_Int1_ITP Vars +imports Abs_Int1_ITP "../Vars" begin instantiation prod :: (preord,preord) preord