ProgTutorial/Intro.thy
changeset 454 e2fe7e93333c
parent 453 bc5c48dc76d0
child 462 1d1e795bc3ad
equal deleted inserted replaced
453:bc5c48dc76d0 454:e2fe7e93333c
   192   or project is of general interest. If you managed to do this, then the
   192   or project is of general interest. If you managed to do this, then the
   193   problem of the moving target goes away, because when checking in new code,
   193   problem of the moving target goes away, because when checking in new code,
   194   developers are strongly urged to test it against Isabelle's code base. If
   194   developers are strongly urged to test it against Isabelle's code base. If
   195   your project is part of that code base, then maintenance is done by
   195   your project is part of that code base, then maintenance is done by
   196   others. Unfortunately, this might not be a helpful advice for all types of
   196   others. Unfortunately, this might not be a helpful advice for all types of
   197   projects. A lower threshold for inclusion has the Archive of Formalised
   197   projects. A lower threshold for inclusion has the Archive of Formal
   198   Proofs, short AFP.\footnote{\url{http://afp.sourceforge.net/}} This archive
   198   Proofs, short AFP.\footnote{\url{http://afp.sourceforge.net/}} This archive
   199   has been created mainly for formalisations that are interesting but not
   199   has been created mainly for formalisations that are interesting but not
   200   necessarily of general interest. If you have ML-code as part of a
   200   necessarily of general interest. If you have ML-code as part of a
   201   formalisation, then this might be the right place for you. There is no
   201   formalisation, then this might be the right place for you. There is no
   202   problem with updating your code after submission. At the moment developers
   202   problem with updating your code after submission. At the moment developers