src/Pure/README

Now Datatype.occs_in_prems prints the necessary warning ITSELF.

It is also easier to invoke and even works if the induction variable
is a parameter (rather than a free variable).

                        Pure: The Pure Isabelle System

This directory contains the ML source files for Pure Isabelle, which is the
basis for all object-logics.  Important files include:

IsaMakefile -- compiles the files

Syntax/     -- the syntax module

Thy/        -- the theory file parser and loader

ML-Systems/ -- compatibility files for various ML systems