src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy

--- a/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy	Thu Feb 20 12:27:51 2014 +1100
+++ b/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy	Wed Feb 19 22:05:05 2014 +0100
@@ -89,7 +89,7 @@
  WHILE b DO lift F c (sub\<^sub>1 ` M)
  {F (post ` M)}"
 
-interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
+permanent_interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
 proof
   case goal1
   have "a:A \<Longrightarrow> lift Inter (strip a) A \<le> a"