# HG changeset patch
# User wenzelm
# Date 966257287 -7200
# Node ID f0e811a54254648ef6ef86f892c6e94225a076e3
# Parent  af21f4364c054dc711301d8854a1f07f32b1d85f
fixed document preparation;

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
 *}
 
diff -r af21f4364c05 -r f0e811a54254 src/HOL/MicroJava/BV/StepMono.thy
--- 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 :