--- a/src/HOL/IMP/Abs_Int3.thy Mon Apr 29 18:52:35 2013 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy Tue Apr 30 03:18:07 2013 +0200
@@ -241,8 +241,8 @@
(metis (mono_tags) strip_iter_widen strip_narrow_acom strip_while)
-locale Abs_Int2 = Abs_Int1_mono
-where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,bounded_lattice} \<Rightarrow> val set"
+locale Abs_Int2 = Abs_Int1_mono where \<gamma>=\<gamma>
+ for \<gamma> :: "'av::{WN,bounded_lattice} \<Rightarrow> val set"
begin
definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
@@ -337,7 +337,8 @@
that not yet @{prop"y \<le> x"}. This complicates the termination proof for
widening. *}
-locale Measure_WN = Measure1 where m=m for m :: "'av::{top,WN} \<Rightarrow> nat" +
+locale Measure_WN = Measure1 where m=m
+ for m :: "'av::{top,WN} \<Rightarrow> nat" +
fixes n :: "'av \<Rightarrow> nat"
assumes m_anti_mono: "x \<le> y \<Longrightarrow> m x \<ge> m y"
assumes m_widen: "~ y \<le> x \<Longrightarrow> m(x \<nabla> y) < m x"
@@ -503,8 +504,7 @@
by blast
qed
-locale Abs_Int2_measure =
- Abs_Int2 where \<gamma>=\<gamma> + Measure_WN where m=m
+locale Abs_Int2_measure = Abs_Int2 where \<gamma>=\<gamma> + Measure_WN where m=m
for \<gamma> :: "'av::{WN,bounded_lattice} \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"