Commit 28c88e82 authored by gerwin.klein@data61.csiro.au's avatar gerwin.klein@data61.csiro.au
Browse files

tweaks to example submission for Isabelle2017

parent 8711e4eaa550
......@@ -60,7 +60,6 @@ Example-Submission/
document/
root.tex
root.bib
config
ROOT
Submission.thy
\end{verbatim}
......@@ -72,9 +71,6 @@ submission should contain title, abstract, author, and any
further documentation
you wish to provide.
The file \texttt{config} contains maintenance information. This is
optional. If you do not submit one, we will create one for you.
\texttt{ROOT} controls which theories should be loaded. If you have
one main theory that depends on all the others, you only need to
include this one. You can also use the \texttt{ROOT} file to control the
......@@ -89,16 +85,7 @@ the article MiniML, the way to import it is:
\begin{verbatim}
theory My_Theory
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 My_Theory
imports "~~/src/HOL/Number_Theory/Number_Theory"
imports MiniML.W
begin
\end{verbatim}
*}
......
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