--- a/src/HOL/IMP/Abs_Int1_parity.thy Thu Feb 20 12:27:51 2014 +1100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Wed Feb 19 22:05:05 2014 +0100
@@ -102,7 +102,7 @@
text{* First we instantiate the abstract value interface and prove that the
functions on type @{typ parity} have all the necessary properties: *}
-interpretation Val_semilattice
+permanent_interpretation Val_semilattice
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
proof txt{* of the locale axioms *}
fix a b :: parity
@@ -123,7 +123,7 @@
proofs (they happened in the instatiation above) but delivers the
instantiated abstract interpreter which we call @{text AI_parity}: *}
-interpretation Abs_Int
+permanent_interpretation Abs_Int
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
defines aval_parity is aval' and step_parity is step' and AI_parity is AI
..
@@ -154,7 +154,7 @@
subsubsection "Termination"
-interpretation Abs_Int_mono
+permanent_interpretation Abs_Int_mono
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
proof
case goal1 thus ?case
@@ -165,7 +165,7 @@
definition m_parity :: "parity \<Rightarrow> nat" where
"m_parity x = (if x = Either then 0 else 1)"
-interpretation Abs_Int_measure
+permanent_interpretation Abs_Int_measure
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
and m = m_parity and h = "1"
proof