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