src/Pure/README
author nipkow
Fri Mar 14 10:35:30 1997 +0100 (1997-03-14)
changeset 2792 6c17c5ec3d8b
parent 19 929ad32d63fc
child 3279 815ef5848324
permissions -rw-r--r--
Avoid eta-contraction in the simplifier.
Instead the net needs to eta-contract the object.
Also added a special function loose_bvar1(i,t) in term.ML.
     1                         Pure: The Pure Isabelle System
     2 
     3 This directory contains the ML source files for Pure Isabelle, which is the
     4 basis for all object-logics.  Important files include:
     5 
     6 Makefile -- compiles the files under Poly/ML or SML of New Jersey
     7 
     8 Syntax/  -- subdirectory containing the syntax module
     9 
    10 Thy/     -- subdirectory containing the thy file parser and loader
    11 
    12 ROOT.ML  -- loads all source files.  Enter ML and type:  use "ROOT.ML";
    13 
    14 NJ.ML    -- compatibility file for Standard ML of New Jersey.  You may wish to
    15             alter the parameter settings.
    16 
    17 POLY.ML  -- compatibility file for Poly/ML
    18