--- a/src/HOL/IMP/Abs_Int1_ivl.thy Sat Dec 31 10:15:53 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1_ivl.thy Sat Dec 31 17:53:50 2011 +0100
@@ -170,7 +170,8 @@
I (max_option False (l1 + Some 1) l2) h2)
else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
-interpretation Val_abs \<gamma>_ivl num_ivl plus_ivl
+interpretation Val_abs
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
defines aval_ivl is aval'
proof
case goal1 thus ?case
@@ -184,7 +185,8 @@
by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split option.splits)
qed
-interpretation Val_abs1_gamma \<gamma>_ivl num_ivl plus_ivl
+interpretation Val_abs1_gamma
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
proof
case goal1 thus ?case
by(auto simp add: \<gamma>_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
@@ -201,8 +203,9 @@
done
-interpretation
- Val_abs1 \<gamma>_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+interpretation Val_abs1
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
proof
case goal1 thus ?case
by(auto simp add: filter_plus_ivl_def)
@@ -213,8 +216,9 @@
auto simp: \<gamma>_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
qed
-interpretation
- Abs_Int1 \<gamma>_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+interpretation Abs_Int1
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
defines afilter_ivl is afilter
and bfilter_ivl is bfilter
and step_ivl is step'
@@ -225,8 +229,9 @@
text{* Monotonicity: *}
-interpretation
- Abs_Int1_mono \<gamma>_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+interpretation Abs_Int1_mono
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
proof
case goal1 thus ?case
by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits)