# HG changeset patch
# User nipkow
# Date 1368160469 -7200
# Node ID 25ceb5fa8f78a498a1518c2c7aedcb9c446bae37
# Parent  e3b7917186f111a33d8e99478611890021e7c996
tuned

diff -r e3b7917186f1 -r 25ceb5fa8f78 src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Thu May 09 20:44:37 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy	Fri May 10 06:34:29 2013 +0200
@@ -134,14 +134,14 @@
 
 end
 
-fun top_on_st :: "'a::top st \<Rightarrow> vname set \<Rightarrow> bool" where
+fun top_on_st :: "'a::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" where
+fun top_on_opt :: "'a::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" where
+definition top_on_acom :: "'a::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"