doc-src/IsarRef/intro.tex
 changeset 11041 e07b601e2b5a parent 10993 883248dcf3f8 child 12618 43a97a2155d0
equal inserted replaced
11040:194406da4e43 11041:e07b601e2b5a
   272   formalization of a fragment of Java, together with a corresponding virtual
   272   formalization of a fragment of Java, together with a corresponding virtual
   273   machine and a specification of its bytecode verifier and a lightweight
   273   machine and a specification of its bytecode verifier and a lightweight
   274   bytecode verifier, including proofs of type-safety.
   274   bytecode verifier, including proofs of type-safety.
   275
   275
   276   This represents a very realistic'' example of large formalizations
   276   This represents a very realistic'' example of large formalizations
   277   performed in either form of legacy scripts, tactic emulation scripts, and
   277   performed in form of tactic emulation scripts and proper Isar proof texts.
   278   proper Isar proof texts.

   279 \end{itemize}
   278 \end{itemize}
   280
   279
   281
   280
   282 %%% Local Variables:
   281 %%% Local Variables:
   283 %%% mode: latex
   282 %%% mode: latex