Commit aa58c129 authored by lsf37's avatar lsf37
Browse files

auto sync with Isabelle2005

parent 1d16de468959
(* Title: An example submission to the Archive of Formal Proof (* Title: An example submission to the Archive of Formal Proof
ID: $Id: Submission.thy,v 1.6 2006-11-09 22:26:13 lsf37 Exp $ ID: $Id: Submission.thy,v 1.7 2006-11-13 15:20:28 lsf37 Exp $
Author: Gerwin Klein <kleing at cse.unsw.edu.au>, 2004 Author: Gerwin Klein <kleing at cse.unsw.edu.au>, 2004
Maintainer: Gerwin Klein <kleing at cse.unsw.edu.au> Maintainer: Gerwin Klein <kleing at cse.unsw.edu.au>
*) *)
...@@ -116,7 +116,7 @@ the article MiniML, the way to import it is: ...@@ -116,7 +116,7 @@ the article MiniML, the way to import it is:
\begin{verbatim} \begin{verbatim}
theory MyTheory theory MyTheory
import "../MiniML/W" imports "../MiniML/W"
begin begin
\end{verbatim} \end{verbatim}
*} *}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment