--- a/src/HOL/IMP/Abs_Int1.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy Thu Jul 25 08:57:16 2013 +0200
@@ -100,7 +100,7 @@
subsubsection "Termination"
locale Measure1 =
-fixes m :: "'av::{order,top} \<Rightarrow> nat"
+fixes m :: "'av::{order,order_top} \<Rightarrow> nat"
fixes h :: "nat"
assumes h: "m x \<le> h"
begin
@@ -134,14 +134,14 @@
end
-fun top_on_st :: "'a::top st \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>s") where
+fun top_on_st :: "'a::order_top st \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>s") where
"top_on_st S X = (\<forall>x\<in>X. fun S x = \<top>)"
-fun top_on_opt :: "'a::top st option \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>o") where
+fun top_on_opt :: "'a::order_top st option \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>o") where
"top_on_opt (Some S) X = top_on_st S X" |
"top_on_opt None X = True"
-definition top_on_acom :: "'a::top st option acom \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>c") where
+definition top_on_acom :: "'a::order_top st option acom \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>c") where
"top_on_acom C X = (\<forall>a \<in> set(annos C). top_on_opt a X)"
lemma top_on_top: "top_on_opt (\<top>::_ st option) X"