Commit cf4f637e authored by gerwin.klein@nicta.com.au's avatar gerwin.klein@nicta.com.au
Browse files

afp.sf.net -> isa-afp.org

parent 5ccf2409c233
......@@ -12,4 +12,4 @@ this repository by sending a request, including your bitbucket login, to
Guidelines for maintaining entries can be found in the `doc/` directory.
[1]: http://afp.sf.net
[1]: http://isa-afp.org
......@@ -2,11 +2,11 @@
#
# Author: Gerwin Klein, NICTA
#
# Cron job that copies development snapshot to SF.
# Cron job that copies development snapshot to isa-afp.org.
#
#SOURCE=~isatest/html-data/afp/
SOURCE=~/afp/web/
TARGET=lsf37,afp@web.sourceforge.net:htdocs/
TARGET=afpweb@isa-afp.org:
/usr/bin/rsync -vrplqz $SOURCE $TARGET
#!/bin/bash
if [ -n "$SF_LOGIN" ]; then
LN=$SF_LOGIN
else
LN=$LOGNAME
fi
TMP=/tmp/releases
ssh $LN,afp@shell.sourceforge.net "ls /home/project-web/afp/htdocs/release" > $TMP
cat $TMP | grep -v "current\\.tar\\.gz\\|devel\\.tar\\.gz\\|entry-status\\.txt\\|afp-....-..-..\\.tar\\.gz\\|afp-Example-Submission-....-..-..\\.tar\\.gz\\|Nominal2.*\\.tar\\.gz"
ssh afpweb@isa-afp.org "ls release" > $TMP
cat $TMP | grep -v "current\\.tar\\.gz\\|devel\\.tar\\.gz\\|entry-status\\.txt\\|afp-....-..-..\\.tar\\.gz\\|afp-Example-Submission-....-..-..\\.tar\\.gz"
......@@ -13,7 +13,7 @@ VERSION=2016
AFP_VERSION=afp-$VERSION
ISABELLE_VERSION=Isabelle$VERSION
DEST=afp@web.sourceforge.net:htdocs/
DEST=afpweb@isa-afp.org:
FILES=frs.sourceforge.net:/home/frs/project/afp/afp-$ISABELLE_VERSION/
SRC=ssh://hg@bitbucket.org/isa-afp/$AFP_VERSION
......@@ -23,7 +23,6 @@ else
LN=$LOGNAME
fi
DEST=$LN,$DEST
FILES=$LN@$FILES
EXPORT_PRE=afp
......@@ -188,10 +187,10 @@ if [ "$RESPONSE" == "y" ]; then
fi
echo
echo "Publishing to [$DEST]"
chmod -R g=u web
chmod -R g-w web
chmod -R a+r web
find web -type d | xargs chmod g+s
find web -type d | xargs chmod a+x
chmod 755 web
rsync -rplvz --links --rsh=ssh web/ $DEST && echo "Finished."
else
echo
......
......@@ -142,7 +142,7 @@ if [ -n "$DIFF" ]; then
The status of the following AFP entries changed or remains FAIL:
$DIFF
Full entry status at http://afp.sourceforge.net/status.shtml
Full entry status at http://isa-afp.org/status.shtml
$AFP_VERSION
$ISA_VERSION
......
......@@ -5,7 +5,7 @@
## Dependencies: Python 2.7 or Python 3.5
##
## This script reads a metadata file and generates the topics.shtml,
## index.shtml and the entry pages on afp.sf.net.
## index.shtml and the entry pages on isa-afp.org.
##
## For meta data documentation see ../metadata/README
## For adding new entries see ../doc/editors/new-entry-checkin.html
......@@ -209,7 +209,7 @@ bibtex_wrapper = u"""@article{{{0}-AFP,
journal = {{Archive of Formal Proofs}},
month = {3},
year = {4},
note = {{\\url{{http://afp.sf.net/entries/{0}.shtml}},
note = {{\\url{{http://isa-afp.org/entries/{0}.shtml}},
Formal proof development}},
ISSN = {{2150-914x}},
}}"""
......@@ -250,8 +250,8 @@ attribute_schema = {
# 'url' contains the url of the license text
licenses = {
'LGPL': ("GNU Lesser General Public License (LGPL)", "http://afp.sourceforge.net/LICENSE.LGPL"),
'BSD': ("BSD License", "http://afp.sourceforge.net/LICENSE"),
'LGPL': ("GNU Lesser General Public License (LGPL)", "http://isa-afp.org/LICENSE.LGPL"),
'BSD': ("BSD License", "http://isa-afp.org/LICENSE"),
}
### template files
......
......@@ -77,7 +77,7 @@ Everything happens in the release branch `afp/release`.
will update the web pages on the server. The script will ask before
it copies, so you can check locally if everything is as you want it.
13. That's it. Changes should show up at <http://afp.sf.net>
13. That's it. Changes should show up at <http://isa-afp.org>
**New submission in devel**
......
......@@ -4,7 +4,7 @@ Maintaining an Entry in the AFP
To maintain an entry, you must have write access to the mercurial
repository of the archive at Bitbucket. To get access, [sign up at
Bitbucket](https://bitbucket.org), and ask one of the
[editors](http://afp.sourceforge.net/about.shtml#editors) to add you to
[editors](http://isa-afp.org/about.shtml#editors) to add you to
the AFP project.
**Setup:**
......
......@@ -1219,7 +1219,7 @@ abstract =
This entry provides executable and verified functional splay trees.
<p>
The amortized complexity of splay trees is analyzed in the AFP entry
<a href="http://afp.sourceforge.net/entries/Amortized_Complexity.shtml">Amortized Complexity</a>.
<a href="http://isa-afp.org/entries/Amortized_Complexity.shtml">Amortized Complexity</a>.
[Skew_Heap]
title = Skew Heap
......@@ -1233,7 +1233,7 @@ abstract =
and verified functional skew heaps.
<p>
The amortized complexity of skew heaps is analyzed in the AFP entry
<a href="http://afp.sourceforge.net/entries/Amortized_Complexity.shtml">Amortized Complexity</a>.
<a href="http://isa-afp.org/entries/Amortized_Complexity.shtml">Amortized Complexity</a>.
[Priority_Queue_Braun]
title = Priority Queues Based on Braun Trees
......@@ -1699,7 +1699,7 @@ abstract =
as infrastructure for Isar-setups.
<p>
This theory is drawn from the
<a href="http://afp.sourceforge.net/entries/Featherweight_OCL.shtml">Featherweight OCL</a>
<a href="http://isa-afp.org/entries/Featherweight_OCL.shtml">Featherweight OCL</a>
project where
it is used to construct a package for object-oriented data-type theories
generated from UML class diagrams. The Featherweight OCL, for example, allows for
......@@ -2859,7 +2859,7 @@ license = LGPL
abstract = This development proves Yoneda's lemma and aims to be readable by humans. It only defines what is needed for the lemma: categories, functors and natural transformations. Limits, adjunctions and other important concepts are not included.
extra-history =
Change history:
[2010-04-23]: The definition of the constant <tt>equinumerous</tt> was slightly too weak in the original submission and has been fixed in revision <a href="http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/8c2b5b3c995f">8c2b5b3c995f</a>.
[2010-04-23]: The definition of the constant <tt>equinumerous</tt> was slightly too weak in the original submission and has been fixed in revision <a href="https://bitbucket.org/isa-afp/afp-devel/commits/8c2b5b3c995f">8c2b5b3c995f</a>.
[Category2]
title = Category Theory
......@@ -3303,7 +3303,7 @@ title = Stream Fusion in HOL with Code Generation
author = Andreas Lochbihler <http://www.infsec.ethz.ch/people/andreloc>, Alexandra Maximova <mailto:amaximov@student.ethz.ch>
date = 2014-10-10
topic = Computer Science/Functional Programming
abstract = Stream Fusion is a system for removing intermediate list data structures from functional programs, in particular Haskell. This entry adapts stream fusion to Isabelle/HOL and its code generator. We define stream types for finite and possibly infinite lists and stream versions for most of the fusible list functions in the theories List and Coinductive_List, and prove them correct with respect to the conversion functions between lists and streams. The Stream Fusion transformation itself is implemented as a simproc in the preprocessor of the code generator. [Brian Huffman's <a href="http://afp.sourceforge.net/entries/Stream-Fusion.shtml">AFP entry</a> formalises stream fusion in HOLCF for the domain of lazy lists to prove the GHC compiler rewrite rules correct. In contrast, this work enables Isabelle's code generator to perform stream fusion itself. To that end, it covers both finite and coinductive lists from the HOL library and the Coinductive entry. The fusible list functions require specification and proof principles different from Huffman's.]
abstract = Stream Fusion is a system for removing intermediate list data structures from functional programs, in particular Haskell. This entry adapts stream fusion to Isabelle/HOL and its code generator. We define stream types for finite and possibly infinite lists and stream versions for most of the fusible list functions in the theories List and Coinductive_List, and prove them correct with respect to the conversion functions between lists and streams. The Stream Fusion transformation itself is implemented as a simproc in the preprocessor of the code generator. [Brian Huffman's <a href="http://isa-afp.org/entries/Stream-Fusion.shtml">AFP entry</a> formalises stream fusion in HOLCF for the domain of lazy lists to prove the GHC compiler rewrite rules correct. In contrast, this work enables Isabelle's code generator to perform stream fusion itself. To that end, it covers both finite and coinductive lists from the HOL library and the Coinductive entry. The fusible list functions require specification and proof principles different from Huffman's.]
[Case_Labeling]
title = Generating Cases from Labeled Subgoals
......
......@@ -35,7 +35,7 @@ entries in the AFP:</p>
<div class="cite">
M. Jaskelioff and S. Merz, Proving the Correctness of Disk
Paxos. <em>Archive of Formal Proofs</em>, June 2005, <a
href="http://afp.sf.net/entries/DiskPaxos.shtml"><tt>http://afp.sf.net/entries/DiskPaxos.shtml</tt></a>, Formal proof development.
href="http://isa-afp.org/entries/DiskPaxos.shtml"><tt>http://isa-afp.org/entries/DiskPaxos.shtml</tt></a>, Formal proof development.
</div>
<p>
......@@ -49,7 +49,7 @@ The bibtext entry for this would be:
journal = {Archive of Formal Proofs},
month = Jun,
year = 2005,
note = {\url{http://afp.sf.net/entries/DiskPaxos.shtml}, Formal proof development},
note = {\url{http://isa-afp.org/entries/DiskPaxos.shtml}, Formal proof development},
ISSN = {2150-914x}
}
</pre>
......
......@@ -76,14 +76,14 @@ automatically and identify exactly the steps that are no longer valid.
journal = {Archive of Formal Proofs},
month = oct,
year = 2014,
note = {\url{http://afp.sf.net/entries/AODV.shtml},
note = {\url{http://isa-afp.org/entries/AODV.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
......
......@@ -59,14 +59,14 @@ Two formalizations of AVL trees with room for extensions. The first formalizatio
journal = {Archive of Formal Proofs},
month = mar,
year = 2004,
note = {\url{http://afp.sf.net/entries/AVL-Trees.shtml},
note = {\url{http://isa-afp.org/entries/AVL-Trees.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -78,14 +78,14 @@ terms and joining processes).</p>
journal = {Archive of Formal Proofs},
month = mar,
year = 2014,
note = {\url{http://afp.sf.net/entries/AWN.shtml},
note = {\url{http://isa-afp.org/entries/AWN.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -65,14 +65,14 @@ refinement proof in the I/O-automata framework of Lynch and Tuttle.
journal = {Archive of Formal Proofs},
month = mar,
year = 2012,
note = {\url{http://afp.sf.net/entries/Abortable_Linearizable_Modules.shtml},
note = {\url{http://isa-afp.org/entries/Abortable_Linearizable_Modules.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -54,14 +54,14 @@ These therories describe Hoare logics for a number of imperative language constr
journal = {Archive of Formal Proofs},
month = aug,
year = 2006,
note = {\url{http://afp.sf.net/entries/Abstract-Hoare-Logics.shtml},
note = {\url{http://isa-afp.org/entries/Abstract-Hoare-Logics.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -72,14 +72,14 @@ instances. <br>
journal = {Archive of Formal Proofs},
month = jun,
year = 2010,
note = {\url{http://afp.sf.net/entries/Abstract-Rewriting.shtml},
note = {\url{http://isa-afp.org/entries/Abstract-Rewriting.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE.LGPL">GNU Lesser General Public License (LGPL)</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE.LGPL">GNU Lesser General Public License (LGPL)</a></td></tr>
<tr><td class="datahead">Depends on:</td>
......
......@@ -54,14 +54,14 @@ The abstract proof can be instantiated for a wide range of Gentzen and tableau s
journal = {Archive of Formal Proofs},
month = apr,
year = 2014,
note = {\url{http://afp.sf.net/entries/Abstract_Completeness.shtml},
note = {\url{http://isa-afp.org/entries/Abstract_Completeness.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
......
......@@ -63,14 +63,14 @@ expression in affine arithmetic.
journal = {Archive of Formal Proofs},
month = feb,
year = 2014,
note = {\url{http://afp.sf.net/entries/Affine_Arithmetic.shtml},
note = {\url{http://isa-afp.org/entries/Affine_Arithmetic.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -67,14 +67,14 @@ proof methods, see the accompanying paper (publication forthcoming).
journal = {Archive of Formal Proofs},
month = jul,
year = 2015,
note = {\url{http://afp.sf.net/entries/Akra_Bazzi.shtml},
note = {\url{http://isa-afp.org/entries/Akra_Bazzi.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
......
......@@ -64,14 +64,14 @@ To this end, we mechanized several results on resultants, which also required us
journal = {Archive of Formal Proofs},
month = dec,
year = 2015,
note = {\url{http://afp.sf.net/entries/Algebraic_Numbers.shtml},
note = {\url{http://isa-afp.org/entries/Algebraic_Numbers.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
......
......@@ -67,14 +67,14 @@ Theorem Proving ITP 2015.
journal = {Archive of Formal Proofs},
month = jul,
year = 2014,
note = {\url{http://afp.sf.net/entries/Amortized_Complexity.shtml},
note = {\url{http://isa-afp.org/entries/Amortized_Complexity.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
......
......@@ -60,14 +60,14 @@ We declare several types from the Isabelle library as applicative functors and i
journal = {Archive of Formal Proofs},
month = dec,
year = 2015,
note = {\url{http://afp.sf.net/entries/Applicative_Lifting.shtml},
note = {\url{http://isa-afp.org/entries/Applicative_Lifting.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -54,14 +54,14 @@ This article formalizes two proofs of Arrow's impossibility theorem due to Geana
journal = {Archive of Formal Proofs},
month = sep,
year = 2008,
note = {\url{http://afp.sf.net/entries/ArrowImpossibilityGS.shtml},
note = {\url{http://isa-afp.org/entries/ArrowImpossibilityGS.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -59,14 +59,14 @@ We formalize the AutoFocus Semantics (a time-synchronous subset of the Focus for
journal = {Archive of Formal Proofs},
month = feb,
year = 2011,
note = {\url{http://afp.sf.net/entries/AutoFocus-Stream.shtml},
note = {\url{http://isa-afp.org/entries/AutoFocus-Stream.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
......
......@@ -66,14 +66,14 @@ the nondeterminism monad and various collection datastructures.
journal = {Archive of Formal Proofs},
month = oct,
year = 2013,
note = {\url{http://afp.sf.net/entries/Automatic_Refinement.shtml},
note = {\url{http://isa-afp.org/entries/Automatic_Refinement.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -53,14 +53,14 @@ We present the verification of the normalisation of a binary decision diagram (B
journal = {Archive of Formal Proofs},
month = feb,
year = 2008,
note = {\url{http://afp.sf.net/entries/BDD.shtml},
note = {\url{http://isa-afp.org/entries/BDD.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
......
......@@ -54,14 +54,14 @@ The correctness is shown of binary search tree operations (lookup, insert and re
journal = {Archive of Formal Proofs},
month = apr,
year = 2004,
note = {\url{http://afp.sf.net/entries/BinarySearchTree.shtml},
note = {\url{http://isa-afp.org/entries/BinarySearchTree.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -67,14 +67,14 @@ operations. Our implementation follows the paper by Brodal and Okasaki.
journal = {Archive of Formal Proofs},
month = oct,
year = 2010,
note = {\url{http://afp.sf.net/entries/Binomial-Heaps.shtml},
note = {\url{http://isa-afp.org/entries/Binomial-Heaps.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -54,14 +54,14 @@ Priority queues are an important data structure and efficient implementations of
journal = {Archive of Formal Proofs},
month = oct,
year = 2010,
note = {\url{http://afp.sf.net/entries/Binomial-Queues.shtml},
note = {\url{http://isa-afp.org/entries/Binomial-Queues.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -53,14 +53,14 @@ A proof of Bondy's theorem following B. Bollabas, Combinatorics, 1986, Cambridge
journal = {Archive of Formal Proofs},
month = oct,
year = 2012,
note = {\url{http://afp.sf.net/entries/Bondy.shtml},
note = {\url{http://isa-afp.org/entries/Bondy.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -64,14 +64,14 @@ the checkers operate on binary decision trees and are reasonably efficient
journal = {Archive of Formal Proofs},
month = jun,
year = 2014,
note = {\url{http://afp.sf.net/entries/Boolean_Expression_Checkers.shtml},
note = {\url{http://isa-afp.org/entries/Boolean_Expression_Checkers.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -60,14 +60,14 @@ which these upper bounds are no longer guaranteed.
journal = {Archive of Formal Proofs},
month = apr,
year = 2014,
note = {\url{http://afp.sf.net/entries/Bounded_Deducibility_Security.shtml},
note = {\url{http://isa-afp.org/entries/Bounded_Deducibility_Security.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -58,14 +58,14 @@ This document contains the Isabelle/HOL sources underlying the paper <i>A byteco
journal = {Archive of Formal Proofs},
month = dec,
year = 2008,
note = {\url{http://afp.sf.net/entries/BytecodeLogicJmlTypes.shtml},
note = {\url{http://isa-afp.org/entries/BytecodeLogicJmlTypes.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......