author | wenzelm |
Fri, 07 Nov 2014 16:22:25 +0100 | |
changeset 58927 | cf47382db395 |
parent 58926 | baf5a3c28f0c |
child 58928 | 23d0ffd48006 |
--- a/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Fri Nov 07 16:13:05 2014 +0100 +++ b/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Fri Nov 07 16:22:25 2014 +0100 @@ -1,5 +1,5 @@ theory Collecting_ITP -imports Complete_Lattice_ix "ACom_ITP" +imports "~~/src/Tools/Permanent_Interpretation" Complete_Lattice_ix "ACom_ITP" begin subsection "Collecting Semantics of Commands"