# HG changeset patch
# User wenzelm
# Date 1415373745 -3600
# Node ID cf47382db395e2d16b76f17d0acdb708dceb5221
# Parent  baf5a3c28f0cfe5c3652406e7c426abad7359174
proper import for command 'permanent_interpretation';

diff -r baf5a3c28f0c -r cf47382db395 src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy
--- 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"