Commit c4378f79 authored by lsf37's avatar lsf37
Browse files

auto sync with Isabelle2005

parent 8af0f4c9653c
(* Title: An example submission to the Archive of Formal Proof
ID: $Id: Submission.thy,v 1.7 2006-11-13 15:20:28 lsf37 Exp $
ID: $Id: Submission.thy,v 1.8 2007-09-02 14:22:19 lsf37 Exp $
Author: Gerwin Klein <kleing at cse.unsw.edu.au>, 2004
Maintainer: Gerwin Klein <kleing at cse.unsw.edu.au>
*)
......@@ -119,6 +119,15 @@ theory MyTheory
imports "../MiniML/W"
begin
\end{verbatim}
To build on a theory that is in the Isabelle distribtion, but not in
one of the standard images like HOL, use something like the following:
\begin{verbatim}
theory MyTheory
imports "~~/src/HOL/NumberTheory"
begin
\end{verbatim}
*}
end
......
Markdown is supported
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