
diff -r af21f4364c05 -r f0e811a54254 src/HOL/MicroJava/BV/Step.thy
--- a/src/HOL/MicroJava/BV/Step.thy	Sat Aug 12 21:42:51 2000 +0200
+++ b/src/HOL/MicroJava/BV/Step.thy	Mon Aug 14 14:48:07 2000 +0200
@@ -84,7 +84,7 @@
 "app (i,G,rT,s)                            = False"
 
 
-text {* \isa{p_count} of successor instructions *}
+text {* \verb,p_count, of successor instructions *}
 
 consts
 succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count set"
@@ -133,8 +133,8 @@
 qed
 
 text {* 
-\mdeskip
-simp rules for \isa{app} without patterns, better suited for proofs
+\medskip
+simp rules for @{term app} without patterns, better suited for proofs
 \medskip
 *}
 




