src/Pure/README

- Moved rewriting functions to meta_simplifier.ML
- dest_abs now also takes an optional variable name as an argument
- beta_conversion takes additional flag as an argument. Fully reduces
the term if set to true

Some tuning:
- tuned fix_shyps in instantiate, implies_intr, implies_elim, reflexive,
transitive, beta_conversion, abstract_rule
- combination: chktypes derives types of f and t from type of == instead
of using fastype_of

New primitives:
- eta_conversion
- incr_indexes: increment indexes in theorems
- cterm_incr_indexes: increment indexes in cterms
- cterm_match, cterm_first_order_match
- rename_boundvars

                        Pure: The Pure Isabelle System


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

  IsaMakefile	compiles the Pure system (use isatool make)
  ML-Systems/   compatibility files for various ML systems
  General/	general tools
  Syntax/     	the syntax module
  Thy/          the theory file parser (old format) and loader
  Isar/		Intelligible Semi-Automated Reasoning subsystem
  ./		the actual meta logic implementation (see ROOT.ML)

Isabelle programmers may want to have a look at the generic modules
Library (see library.ML) and those in General/ (see General/README).