Commit d0563fe9 authored by lsf37's avatar lsf37
Browse files

import to SF

parent dce145e81ab1
## configurables
SESSION-NAME = Example-Submission
BASE-IMAGE = HOL
# turn image into absolute path when ISABELLE_IMAGE_PATH is set
IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
## targets
default: $(SESSION-NAME)
test: $(SESSION-NAME)
# usually empty:
images:
all: images test
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
USEDIR = $(ISATOOL) usedir -v true -i true -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
## dependencies
$(SESSION-NAME): $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
$(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz: ROOT.ML *.thy document/*.tex document/*.bib
cd ..; $(USEDIR) $(IMAGE) $(SESSION-NAME)
## clean
clean:
@rm -f $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
(* if you'd like to build on other archive entries (here "Example"), use:
add_path "../Example";
*)
(* to suppress document generation of some theories, use:
no_document use_thy "ThisTheory";
*)
(* for normal theory loading, use:
use_thy "ThatTheory";
*)
use_thy "Submission";
(* Title: An example submission to the Archive of Formal Proof
ID: $Id: Submission.thy,v 1.1 2004-02-25 02:49:35 lsf37 Exp $
Author: Gerwin Klein <kleing@cse.unsw.edu.au>, 2004
Maintainer: Gerwin Klein <kleing@cse.unsw.edu.au>
License: LGPL
*)
header "An Example Submission"
theory Submission = Main:
text {*
This is an example submission to the Archive of Formal Proof.
The scope of the archive encompasses examples, textbook-style
proofs, libraries and larger scientific developments.
*}
section "Format of a submission"
text {*
Submission should be by email to \url{afp-submit@in.tum.de} and contain
the following:
\begin{itemize}
\item Title, authors, and abstract.
The abstract should be in plain text or plain html (no images/styles).
\item A short name that will become the directory name of the
submission.
\item The Isabelle theories: a tar.gz file with the theory files,
ROOT.ML, and a README file or document directory.
The theories should work with the current release of Isabelle.
Each theory file should include a header comment like the one
in this theory.
\item A statement that submission your is licenced under LGPL.
\end{itemize}
The submission of the example you are reading is at
\url{insert-example-tar-gz-url}.
*}
section "Proof styles"
text {*
We accept proofs in \isakeyword{apply}-script style like the
following.
*}
lemma true: "True"
apply blast
done
text {*
We encourage structured proofs with comments and
explanations. The Isabelle document preparation tools support
antiquotations like @{thm true}, normal {\LaTeX} commands and BibTeX
citations. See \cite{LNCS2283} and the Isabelle documentation for
more information.
*}
lemma very_true: "True"
proof -
-- "a very roundabout way"
have "P \<longrightarrow> True" by blast
-- "to show @{term True}"
thus True by blast
qed
section "The anatomy of a submission"
text {*
The directory structure of this example submission is the following
\begin{verbatim}
Example-Submission/
document/
root.tex
root.bib
config
IsaMakefile
ROOT.ML
README.html
Submission.thy
\end{verbatim}
The document directory contains the {\LaTeX} master file
\texttt{root.tex} and the bibliography \texttt{root.bib}. Your
submission should contain this {\LaTeX} setup or a \texttt{README.html}
(or both) with title, abstract, author, and any further documentation
you whish to provide. We encourage {\LaTeX} style documentation over
\texttt{README.html}.
The file \texttt{config} contains maintenance information. This is
optional. If you do not submit one, we will create one for you.
The \texttt{IsaMakefile} tells the automated build scripts how to test
your Isabelle theories. For a usual setup you only need to copy the
version from this example and adjust the variable
\texttt{SESSION-NAME}. If you need support with this, please contact
us or ask on the \texttt{isabelle-users} mailing list.
\texttt{ROOT.ML} 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 \texttt{ROOT.ML} to control the
order in which theories are read. If you would like to build on other
entries in the archive, which we enourage, you can use the
\texttt{add\_path} command in \texttt{ROOT.ML} to add the directory of
the other entry to the theory search path. See the \texttt{ROOT.ML} of
this submission for an example.
The file \texttt{Submission.thy} is the Isabelle theory containing
this text. A usual submission has more than one theory file. You can
devise your own subdirectory structure if you have more theories and
one directory becomes too crowded.
*}
end
\ No newline at end of file
# -*- shell-script -*-
# $Id: config,v 1.1 2004-02-25 02:49:35 lsf37 Exp $
# Get email when automated build fails. May be empty.
# values: "email1 email2 .. emailn"
NOTIFY="kleing@cse.unsw.edu.au"
# Participate in frequent (nightly) build (only for small submissions)
# values: "yes" "no"
FREQUENT="yes"
@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
publisher=Springer,series=LNCS,volume=2283,year=2002,
note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}
% $Id: root.tex,v 1.1 2004-02-25 02:49:35 lsf37 Exp $
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
% further packages required for unusual symbols (see also isabellesym.sty)
% use only when needed
%\usepackage{amssymb} % for \<leadsto>, \<box>, \<diamond>,
% \<sqsupset>, \<mho>, \<Join>,
% \<lhd>, \<lesssim>, \<greatersim>,
% \<lessapprox>, \<greaterapprox>,
% \<triangleq>, \<yen>, \<lozenge>
%\usepackage[greek,english]{babel} % greek for \<euro>,
% english for \<guillemotleft>,
% \<guillemotright>
% default language = last
%\usepackage[latin1]{inputenc} % for \<onesuperior>, \<onequarter>,
% \<twosuperior>, \<onehalf>,
% \<threesuperior>, \<threequarters>,
% \<degree>
%\usepackage[only,bigsqcap]{stmaryrd} % for \<Sqinter>
%\usepackage{eufrak} % for \<AA> ... \<ZZ>, \<aa> ... \<zz>
% (only needed if amssymb not used)
%\usepackage{textcomp} % for \<cent>, \<currency>
% this should be the last package used
\usepackage{pdfsetup}
% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}
\begin{document}
\title{Submission Example}
\author{Gerwin Klein}
\maketitle
\begin{abstract}
This is an example submission to the Archive of Formal Proof. It
shows submission requirements and explains the structure of a simple
typical submission.
\end{abstract}
\tableofcontents
\parindent 0pt\parskip 0.5ex
% include generated text of all theories
\input{session}
\bibliographystyle{abbrv}
\bibliography{root}
\end{document}
h1 {
font: normal small-caps bold large sans-serif;
color: white;
background: #2e2d4e;
padding-top: 10px;
padding-right: 10px;
padding-bottom: 10px;
padding-left: 10px;
border-width: thin thin thin thin;
border-style: none none none none;
}
h1 font.first {
font: normal normal bold x-large sans-serif;
}
table.nav {
font: normal normal bold medium sans-serif;
background-color: lightGray;
border-width: thin thin thin thin;
border-style: solid solid solid solid;
width: 80%;
display: block;
;
}
table.nav a:link { font-weight:bold; color:#000000; text-decoration:none }
table.nav a:visited { font-weight:bold; color:#000000; text-decoration:none }
table.nav a:hover { font-weight:bold; color:#000080; text-decoration:underline }
table.nav a:active { font-weight:bold; color:#000000; text-decoration:underline
}
table.nav a:focus { font-weight:bold; color:#000000; text-decoration:underline }
td.nav {
background-color: white;
margin-top: 20px;
margin-right: 20px;
margin-bottom: 20px;
margin-left: 20px;
padding-top: 5px;
padding-right: 5px;
padding-bottom: 5px;
padding-left: 5px;
border-width: thin thin thin thin;
border-style: none none none none;
;
}
table.descr {
font: normal normal normal medium sans-serif;
background-color: lightGray;
padding: 2ex 2ex 2ex 2ex;
border-width: thin thin thin thin;
border-style: solid solid solid solid;
;
}
td.descr {
font: normal normal normal medium sans-serif;
background-color: lightGray;
padding: 2ex 2ex 2ex 2ex;
;
}
table.entries {
font: normal normal normal medium sans-serif;
background-color: lightGray;
border-width: thin thin thin thin;
border-style: solid solid solid solid;
;
}
td.head {
font: normal normal bold medium sans-serif;
color: #E2E2E2;
background-color: #2e2d4e;
word-spacing: normal;
letter-spacing: normal;
text-decoration: none;
word-spacing: normal;
vertical-alignment: baseline;
text-transformation: none;
text-alignment: left;
text-indentation: 2em;
line-height: normal;
margin: 1em 1em 1em 0em;
padding: 0.5ex 0.5ex 0.5ex 0.5ex;
border-width: thin thin thin thin;
border-style: none none none none;
width: 95%;
height: auto;
float: left;
clear: none;
display: block;
white-space: normal;
list-style-position: inside;
;
}
td.entry {
font: normal normal normal medium sans-serif;
color: black;
background-color: #E2E2E2;
word-spacing: normal;
letter-spacing: normal;
text-decoration: none;
word-spacing: normal;
vertical-alignment: baseline;
text-transformation: none;
text-alignment: left;
text-indentation: 2em;
line-height: normal;
margin: 0em 1em 1em 5%;
padding: 0.5ex 0.5ex 0.5ex 0.5ex;
border-width: thin thin thin thin;
border-style: none none none none;
width: 90%;
height: auto;
float: left;
clear: none;
display: block;
white-space: normal;
list-style-position: inside;
;
}
table.data {
margin: 0em 0em 0em 0em;
padding: 0.5ex 0.5ex 0.5ex 0.5ex;
border-width: thin thin thin thin;
border-style: solid solid solid solid;
;
}
td.datahead {
font: normal normal bold medium sans-serif;
color: black;
background-color: #E2E2E2;
margin: 1em 1em auto 0em;
padding: 0.5ex 0.5ex 0.5ex 0.5ex;
border-width: thin thin thin thin;
border-style: none none none none;
;
}
td.data {
font: normal normal normal medium sans-serif;
color: black;
background-color: #E2E2E2;
margin: 1em 1em auto 0em;
padding: 0.5ex 0.5ex 0.5ex 0.5ex;
border-width: thin thin thin thin;
border-style: none none none none;
;
}
td.abstract {
font: normal normal normal medium sans-serif;
color: black;
background-color: #E2E2E2;
margin: 1em 1em auto 0em;
padding: 0.5ex 0.5ex 0.5ex 0.5ex;
border-width: thin thin thin thin;
border-style: none none none none;
;
}
table.links {
margin: 0em 0em 0em 0em;
padding: 0.5ex 0.5ex 0.5ex 0.5ex;
border-width: thin thin thin thin;
border-style: solid solid solid solid;
;
}
td.links {
font: normal normal normal medium sans-serif;
color: black;
background-color: #E2E2E2;
margin: 1em 1em 0em 0em;
padding: 0.5ex 0.5ex 0.5ex 0.5ex;
border-width: thin thin thin thin;
border-style: none none none none;
;
}
div.date {
font-family: sans-serif;
font-size: small;
color: black;
margin-top: 5ex;
padding-top: 1ex;
border-width: thin thin thin thin;
border-style: none none none none;
width: 100%;
}
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