File	Date	Author	Commit
document	2017-07-11	Joachim Breitner	[701778] Spelling
etc	2013-05-10	Christian Sternagel	[3dfeaa] initial setup for document preparation; more un...
examples	2017-07-11	Joachim Breitner	[c0ddd4] Add missing section titles and text
paper	2017-07-11	Christian Sternagel	[ca2ae3] modernizations: isabelle update_{cartouches -t ...
translate	2013-05-28	Neil Mitchell	[d0cc9a] Initial version of a Haskell/HLint translation ...
.hgignore	2013-05-03	Christian Sternagel	[bcd262] added initial version of extended abstract (sho...
.hgtags	2013-06-06	Christian Sternagel	[0f96a4] Added tag HART2013-final for changeset bfd29ec5...
COMPATIBILITY	2014-10-10	Christian Sternagel	[abf0b8] adapted to Isabelle2014 (except for Sieve_Prime...
Data_Bool.thy	2017-07-11	Christian Sternagel	[8dc0ee] tuned layout
Data_Function.thy	2017-07-11	Christian Sternagel	[8dc0ee] tuned layout
Data_Integer.thy	2017-07-11	Christian Sternagel	[05814f] tuned layout
Data_List.thy	2017-07-11	Christian Sternagel	[8dc0ee] tuned layout
Data_Maybe.thy	2017-07-11	Christian Sternagel	[8dc0ee] tuned layout
Data_Tuple.thy	2017-07-11	Christian Sternagel	[05814f] tuned layout
Definedness.thy	2017-07-11	Christian Sternagel	[05814f] tuned layout
HOLCF_Main.thy	2017-07-11	Christian Sternagel	[05814f] tuned layout
HOLCF_Prelude.thy	2017-07-11	Christian Sternagel	[05814f] tuned layout
List_Comprehension.thy	2017-07-11	Christian Sternagel	[05814f] tuned layout
Num_Class.thy	2017-07-11	Christian Sternagel	[05814f] tuned layout
Numeral_Cpo.thy	2017-07-11	Christian Sternagel	[05814f] tuned layout
README	2014-10-10	Christian Sternagel	[abf0b8] adapted to Isabelle2014 (except for Sieve_Prime...
ROOT	2017-07-11	Joachim Breitner	[c0ddd4] Add missing section titles and text
ROOTS	2013-02-14	Christian Sternagel	[82bacd] more conventional session setup (per directory ...
Type_Classes.thy	2017-07-11	Christian Sternagel	[8dc0ee] tuned layout

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/)