changeset 49095 | 7df19036392e |
parent 48759 | ff570720ba1c |
child 52046 | bc01725d7918 |
--- a/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Mon Sep 03 09:15:58 2012 +0200 +++ b/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Mon Sep 03 15:41:06 2012 +0200 @@ -1,5 +1,5 @@ theory Collecting_ITP -imports Complete_Lattice_ix "../ACom" +imports Complete_Lattice_ix "ACom_ITP" begin subsection "Collecting Semantics of Commands"