# HG changeset patch
# User wenzelm
# Date 1312735116 -7200
# Node ID 2ff2a54d0fb5193538aa5cf7b05df695cda2087e
# Parent  01d6ab227069df173d208ec3650351d4f5af2b1a
fixed document;

diff -r 01d6ab227069 -r 2ff2a54d0fb5 src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Fri Aug 05 23:06:54 2011 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Sun Aug 07 18:38:36 2011 +0200
@@ -52,7 +52,7 @@
 definition raise_if :: "bool \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option" where
   "raise_if b x xo \<equiv> if b \<and>  (xo = None) then Some (Addr (XcptRef x)) else xo"
 
-text {* Make new_Addr completely specified (at least for the code generator) *}
+text {* Make @{text new_Addr} completely specified (at least for the code generator) *}
 (*
 definition new_Addr  :: "aheap => loc \<times> val option" where
   "new_Addr h \<equiv> SOME (a,x). (h a = None \<and>  x = None) |  x = Some (Addr (XcptRef OutOfMemory))"