diff -r bc5c48dc76d0 -r e2fe7e93333c ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Fri Oct 29 12:57:44 2010 +0200 +++ b/ProgTutorial/Intro.thy Fri Oct 29 13:00:33 2010 +0200 @@ -194,7 +194,7 @@ developers are strongly urged to test it against Isabelle's code base. If your project is part of that code base, then maintenance is done by others. Unfortunately, this might not be a helpful advice for all types of - projects. A lower threshold for inclusion has the Archive of Formalised + projects. A lower threshold for inclusion has the Archive of Formal Proofs, short AFP.\footnote{\url{http://afp.sourceforge.net/}} This archive has been created mainly for formalisations that are interesting but not necessarily of general interest. If you have ML-code as part of a