src/HOL/IMP/Abs_State.thy
changeset 49577 b199aa1d33fd
parent 49497 860b7c6bd913
child 50995 3371f5ee4ace
--- a/src/HOL/IMP/Abs_State.thy	Tue Sep 25 07:37:42 2012 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Wed Sep 26 02:51:59 2012 +0200
@@ -60,7 +60,7 @@
 end
 
 class semilatticeL = join + L +
-fixes top :: "com \<Rightarrow> 'a" ("\<top>\<^bsub>_\<^esub>")
+fixes top :: "com \<Rightarrow> 'a"
 assumes join_ge1 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<sqsubseteq> x \<squnion> y"
 and join_ge2 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> y \<sqsubseteq> x \<squnion> y"
 and join_least[simp]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
@@ -68,6 +68,8 @@
 and top_in_L[simp]: "top c \<in> L(vars c)"
 and join_in_L[simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<squnion> y \<in> L X"
 
+notation (input) top ("\<top>\<^bsub>_\<^esub>")
+notation (latex output) top ("\<top>\<^bsub>\<^raw:\isa{>_\<^raw:}>\<^esub>")
 
 instantiation option :: (semilatticeL)semilatticeL
 begin