Learn how easy it is to sync an existing GitHub or Google Code repo to a SourceForge project! See Demo

Close

Tree [abf0b8] default tip /
History



File Date Author Commit
document 2013-05-10 Christian Sternagel Christian Sternagel [9b07de] forgot to add document files (process document ...
etc 2013-05-10 Christian Sternagel Christian Sternagel [3dfeaa] initial setup for document preparation; more un...
examples 2014-10-10 Christian Sternagel Christian Sternagel [abf0b8] adapted to Isabelle2014 (except for Sieve_Prime...
paper 2013-06-05 Christian Sternagel Christian Sternagel [bfd29e] updated hlint version
translate 2013-05-28 Neil Mitchell Neil Mitchell [d0cc9a] Initial version of a Haskell/HLint translation ...
.hgignore 2013-05-03 Christian Sternagel Christian Sternagel [bcd262] added initial version of extended abstract (sho...
.hgtags 2013-06-06 Christian Sternagel Christian Sternagel [0f96a4] Added tag HART2013-final for changeset bfd29ec5...
COMPATIBILITY 2014-10-10 Christian Sternagel Christian Sternagel [abf0b8] adapted to Isabelle2014 (except for Sieve_Prime...
Data_Bool.thy 2013-05-10 Christian Sternagel Christian Sternagel [3dfeaa] initial setup for document preparation; more un...
Data_Function.thy 2013-05-10 Christian Sternagel Christian Sternagel [3dfeaa] initial setup for document preparation; more un...
Data_Integer.thy 2014-10-10 Christian Sternagel Christian Sternagel [abf0b8] adapted to Isabelle2014 (except for Sieve_Prime...
Data_List.thy 2014-10-10 Christian Sternagel Christian Sternagel [abf0b8] adapted to Isabelle2014 (except for Sieve_Prime...
Data_Maybe.thy 2013-05-10 Christian Sternagel Christian Sternagel [3dfeaa] initial setup for document preparation; more un...
Data_Tuple.thy 2013-05-10 Christian Sternagel Christian Sternagel [3dfeaa] initial setup for document preparation; more un...
Definedness.thy 2014-10-10 Christian Sternagel Christian Sternagel [abf0b8] adapted to Isabelle2014 (except for Sieve_Prime...
HOLCF_Main.thy 2013-05-10 Christian Sternagel Christian Sternagel [3dfeaa] initial setup for document preparation; more un...
HOLCF_Prelude.thy 2013-05-04 Christian Sternagel Christian Sternagel [d126d5] added theory HOLCF_Prelude (as common entry poi...
List_Comprehension.thy 2014-10-10 Christian Sternagel Christian Sternagel [abf0b8] adapted to Isabelle2014 (except for Sieve_Prime...
Num_Class.thy 2013-05-10 Christian Sternagel Christian Sternagel [3dfeaa] initial setup for document preparation; more un...
Numeral_Cpo.thy 2014-10-10 Christian Sternagel Christian Sternagel [abf0b8] adapted to Isabelle2014 (except for Sieve_Prime...
README 2014-10-10 Christian Sternagel Christian Sternagel [abf0b8] adapted to Isabelle2014 (except for Sieve_Prime...
ROOT 2014-10-10 Christian Sternagel Christian Sternagel [abf0b8] adapted to Isabelle2014 (except for Sieve_Prime...
ROOTS 2013-02-14 Christian Sternagel Christian Sternagel [82bacd] more conventional session setup (per directory ...
Type_Classes.thy 2013-06-04 Christian Sternagel Christian Sternagel [82ff51] comment

Read Me

To obtain a specific version of the HOLCF-Prelude repository use:

  hg clone -r <version> http://hg.code.sf.net/p/holcf-prelude/code holcf-prelude

or after cloning

  hg update -r <version>

where <version> is of the form "v<major>.<minor>" (e.g., "v0.1" for version
0.1).

We assume a working Isabelle installation (consult the file COMPATIBILITY for
version information). Installation instructions for Isabelle can be found at one
of the following places:

  Cambridge (UK)      http://www.cl.cam.ac.uk/research/hvg/Isabelle/
  Munich (Germany)    http://isabelle.in.tum.de/
  Sydney (Australia)  http://mirror.cse.unsw.edu.au/pub/isabelle/ 

To check everything (the prelude and all examples), from inside the
root-directory of the Isabelle/HOLCF standard prelude, run

  isabelle build -D .

When working on any HOLCF-Prelude theory, start Isabelle/jEdit via

  isabelle jedit -l HOLCF <theory-file>

When working on examples use

  isabelle jedit -d . -l HOLCF-Prelude <theory-file>

This will automatically build any required heap images. (Note that in the latter
case you will not be able to modify theories from HOLCF-Prelude, since those are
already part of a finished heap image.)

Available sessions:

  - HOLCF-Prelude: build the HOLCF prelude; subsequently import HOLCF_Prelude in
    your theories

  - HOLCF-Prelude-Experimental: as above, but also build experimental parts of
    the prelude

  - HOLCF-Prelude-Examples: build accompanying examples (in subdirectory
    examples/)