| changeset 11041 | e07b601e2b5a |
| parent 10993 | 883248dcf3f8 |
| child 12618 | 43a97a2155d0 |
--- a/doc-src/IsarRef/intro.tex Sat Feb 03 00:01:54 2001 +0100 +++ b/doc-src/IsarRef/intro.tex Sat Feb 03 00:11:07 2001 +0100 @@ -274,8 +274,7 @@ bytecode verifier, including proofs of type-safety. This represents a very ``realistic'' example of large formalizations - performed in either form of legacy scripts, tactic emulation scripts, and - proper Isar proof texts. + performed in form of tactic emulation scripts and proper Isar proof texts. \end{itemize}