--- 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
*}