Commit 86a2a19b authored by nipkow's avatar nipkow
Browse files

dropped The in front of Archive.

parent 0e83d21a4302
......@@ -2,7 +2,7 @@
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>The Archive of Formal Proofs</title>
<title>Archive of Formal Proofs</title>
<link rel="stylesheet" type="text/css" href="front.css">
<link rel="icon" href="images/favicon.ico" type="image/icon">
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
......
......@@ -2,7 +2,7 @@
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>The Archive of Formal Proofs</title>
<title>Archive of Formal Proofs</title>
<link rel="stylesheet" type="text/css" href="front.css">
<link rel="icon" href="images/favicon.ico" type="image/icon">
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
......
......@@ -2,7 +2,7 @@
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>The Archive of Formal Proofs - Index by Topic</title>
<title>Archive of Formal Proofs - Index by Topic</title>
<link rel="stylesheet" type="text/css" href="front.css">
<link rel="icon" href="images/favicon.ico" type="image/icon">
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
......
......@@ -64,7 +64,7 @@
@incollection{L09_collections,
author = {Peter Lammich},
title = {Collections Framework},
booktitle = {The Archive of Formal Proofs},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sf.net/entries/collections.shtml}},
month = Dec,
......@@ -76,7 +76,7 @@
@incollection{L09_tree_automata,
author = {Peter Lammich},
title = {Tree Automata},
booktitle = {The Archive of Formal Proofs},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sf.net/entries/Tree-Automata.shtml}},
month = Dec,
......@@ -88,7 +88,7 @@
@incollection{NKP10,
author = {Benedikt Nordhoff and Stefan K{\"o}rner and Peter Lammich},
title = {Finger Trees},
booktitle = {The Archive of Formal Proofs},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sf.net/entries/Tree-Automata.shtml}},
month = Oct,
......
(* Title: An example submission to the Archive of Formal Proof
(* Title: An example submission to the Archive of Formal Proofs
Author: Gerwin Klein <kleing at cse.unsw.edu.au>, 2004
Maintainer: Gerwin Klein <kleing at cse.unsw.edu.au>
*)
......@@ -10,7 +10,7 @@ theory Submission
begin
text {*
This is an example submission to the Archive of Formal Proof.
This is an example submission to the Archive of Formal Proofs.
The scope of the archive encompasses examples, textbook-style
proofs, libraries and larger scientific developments.
......
......@@ -38,7 +38,7 @@
\maketitle
\begin{abstract}
This is an example submission to the Archive of Formal Proof. It
This is an example submission to the Archive of Formal Proofs. It
shows submission requirements and explains the structure of a simple
typical submission.
\end{abstract}
......
......@@ -208,7 +208,7 @@ institution="{TUCS}"
@incollection{preoteasa:back:afp:2010,
author = {Viorel Preoteasa and Ralph-Johan Back},
title = {Semantics and Data Refinement of Invariant Based Programs},
booktitle = {The Archive of Formal Proofs},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sf.net/entries/DataRefinementIBP.shtml}},
month = May,
......
......@@ -77,7 +77,7 @@ Thomas Reps and Susan Horwitz and Mooly Sagiv and Genevieve Rosay.
\bibitem{Wasserrab:08}
\newblock Daniel Wasserrab.
\newblock Towards certified slicing.
\newblock In G. Klein, T. Nipkow, and L. Paulson, editors, {\em The Archive of Formal
\newblock In G. Klein, T. Nipkow, and L. Paulson, editors, {\em Archive of Formal
Proofs}.
\newblock \url{http://afp.sf.net/entries/Slicing.shtml}, September 2008.
\newblock Formal proof development.
......
@INCOLLECTION{Wasserrab:08,
author = {Daniel Wasserrab},
title = {Towards Certified Slicing},
booktitle = {The Archive of Formal Proofs},
booktitle = {Archive of Formal Proofs},
publisher = {\url{http://afp.sf.net/entries/Slicing.shtml}},
year = {2008},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
......@@ -13,7 +13,7 @@
@INCOLLECTION{Wasserrab:09,
author = {Daniel Wasserrab},
title = {Backing up Slicing: Verifying the Interprocedural Two-Phase {H}orwitz-{R}eps-{B}inkley Slicer},
booktitle = {The Archive of Formal Proofs},
booktitle = {Archive of Formal Proofs},
publisher = {\url{http://afp.sf.net/entries/HRB-Slicing.shtml}},
year = {2009},
OPTeditor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
......@@ -70,7 +70,7 @@
@INCOLLECTION{BeringerH:08,
author = {Lennart Beringer and Martin Hofmann},
title = {Secure information flow and program logics},
booktitle = {The Archive of Formal Proofs},
booktitle = {Archive of Formal Proofs},
publisher = {\url{http://afp.sf.net/entries/SIFPL.shtml}},
year = {2008},
OPTeditor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
......@@ -82,7 +82,7 @@
@INCOLLECTION{SneltingW:08,
author = {Gregor Snelting and Daniel Wasserrab},
title = {A Correctness Proof for the {Volpano/Smith} Security Typing System},
booktitle = {The Archive of Formal Proofs},
booktitle = {Archive of Formal Proofs},
publisher = {\url{http://afp.sf.net/entries/VolpanoSmith.shtml}},
year = {2008},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
......
......@@ -257,7 +257,7 @@ results are formalized and mechanically proved in the Isabelle/HOL theorem prove
@incollection{preoteasa:back:2010a,
author = {Preoteasa, Viorel and Back, Ralph-Johan},
title = {Semantics and Data Refinement of Invariant Based Programs },
booktitle = {The Archive of Formal Proofs},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {http://afp.sourceforge.net/entries/DataRefinementIBP.shtml},
month = May,
......@@ -269,7 +269,7 @@ results are formalized and mechanically proved in the Isabelle/HOL theorem prove
@incollection{preoteasa:back:2010b,
author = {Preoteasa, Viorel and Back, Ralph-Johan},
title = {Verification of the {D}eutsch-{S}chorr-{W}aite Graph Marking Algorithm using Data Refinement},
booktitle = {The Archive of Formal Proofs},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {http://afp.sourceforge.net/entries/GraphMarkingIBP.shtml},
month = May,
......
......@@ -76,7 +76,7 @@
@incollection{L09_collections,
author = {Peter Lammich},
title = {Collections Framework},
booktitle = {The Archive of Formal Proofs},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sf.net/entries/collections.shtml}},
month = Dec,
......@@ -88,7 +88,7 @@
@incollection{L09_tree_automata,
author = {Peter Lammich},
title = {Tree Automata},
booktitle = {The Archive of Formal Proofs},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sf.net/entries/Tree-Automata.shtml}},
month = Dec,
......
......@@ -69,7 +69,7 @@
@incollection{Nipkow-AFP-AHL,
author = {Tobias Nipkow},
title = {Abstract {H}oare Logics},
booktitle = {The Archive of Formal Proofs},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sourceforge.net/entries/Abstract-Hoare-Logics.shtml}},
month = Jun,
......
......@@ -72,7 +72,7 @@
@incollection{Nipkow:2008,
author = {Tobias Nipkow},
title = {{Arrow and Gibbard-Satterthwaite}},
booktitle = {The Archive of Formal Proofs},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sourceforge.net/devel-entries/ArrowImpossibilityGS.shtml}},
month = Sep,
......
@incollection{rtrancl_fin,
author={C.~Sternagel and R.~Thiemann},
title={{Executable} {Transitive} {Closures} of {Finite} {Relations}},
booktitle={The Archive of Formal Proofs},
booktitle={Archive of Formal Proofs},
publisher={\url{http://afp.sf.net/entries/Transitive-Closure.shtml}},
month=mar,
year=2011,
......
......@@ -11,7 +11,7 @@
@incollection{L09_collections,
author = {Peter Lammich},
title = {Isabelle Collection Library},
booktitle = {The Archive of Formal Proofs},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sf.net/entries/collections.shtml}},
month = Dez,
......
......@@ -2,7 +2,7 @@
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>The Archive of Formal Proofs</title>
<title>Archive of Formal Proofs</title>
<link rel="stylesheet" type="text/css" href="front.css">
<link rel="icon" href="images/favicon.ico" type="image/icon">
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
......@@ -74,7 +74,7 @@ understand details of your development, and it makes it easier to use and
build on your work.</p>
<h2>License</h2>
<p>All entries in the Archive of Formal Proof are licensed under
<p>All entries in the Archive of Formal Proofs are licensed under
a <a href="LICENSE">BSD-style License</a> or
the <a href="http://www.gnu.org/copyleft/lesser.html">GNU LGPL</a>.
This means they are free to download, free to use, free to change, and
......
......@@ -2,7 +2,7 @@
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>The Archive of Formal Proofs</title>
<title>Archive of Formal Proofs</title>
<link rel="stylesheet" type="text/css" href="front.css">
<link rel="icon" href="images/favicon.ico" type="image/icon">
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
......@@ -34,7 +34,7 @@ entries in the AFP:</p>
<div class="cite">
M. Jaskelioff and S. Merz, <em>Proving the Correctness of Disk
Paxos</em>. In: G. Klein, T. Nipkow, and L. Paulson (ed), The Archive
Paxos</em>. In: G. Klein, T. Nipkow, and L. Paulson (ed), Archive
of Formal Proofs, <a
href="http://afp.sf.net/entries/DiskPaxos.shtml"><tt>http://afp.sf.net/entries/DiskPaxos.shtml</tt></a>,
June 2005, Formal proof development.
......@@ -48,7 +48,7 @@ The bibtext entry for this would be:
@incollection{Jaskelioff-Merz-AFP05,
author = {Mauro Jaskelioff and Stephan Merz},
title = {Proving the Correctness of Disk Paxos},
booktitle = {The Archive of Formal Proofs},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sf.net/entries/DiskPaxos.shtml}},
month = Jun,
......
......@@ -2,7 +2,7 @@
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>The Archive of Formal Proofs</title>
<title>Archive of Formal Proofs</title>
<link rel="stylesheet" type="text/css" href="front.css">
<link rel="icon" href="images/favicon.ico" type="image/icon">
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
......
......@@ -2,7 +2,7 @@
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>The Archive of Formal Proofs</title>
<title>Archive of Formal Proofs</title>
<link rel="stylesheet" type="text/css" href="front.css">
<link rel="icon" href="images/favicon.ico" type="image/icon">
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
......
......@@ -2,7 +2,7 @@
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>The Archive of Formal Proofs</title>
<title>Archive of Formal Proofs</title>
<link rel="stylesheet" type="text/css" href="front.css">
<link rel="icon" href="images/favicon.ico" type="image/icon">
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
......
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