| changeset 9585 | f0e811a54254 |
| parent 9580 | d955914193e0 |
| child 9594 | 42d11e0a7a8b |
--- 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 :