--- 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
*}
--- a/src/HOL/MicroJava/BV/StepMono.thy Sat Aug 12 21:42:51 2000 +0200
+++ b/src/HOL/MicroJava/BV/StepMono.thy Mon Aug 14 14:48:07 2000 +0200
@@ -4,7 +4,7 @@
Copyright 2000 Technische Universitaet Muenchen
*)
-header {* Monotonicity of \isa{step} and \isa{app} *}
+header {* Monotonicity of \texttt{step} and \texttt{app} *}
theory StepMono = Step :