# HG changeset patch
# User nipkow
# Date 1348620719 -7200
# Node ID b199aa1d33fd2cc5ab1fa004f8fd8fb100b91d0b
# Parent  6abbede3ae128e13afddc8638be3d390401a98cc
tuned

diff -r 6abbede3ae12 -r b199aa1d33fd src/HOL/IMP/Abs_State.thy
--- 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