Removed exception handlers, as they are now in ZF/Makefile.

Now calls exit_use instead of use, for prompt failure if errors are detected.

Declares the function exit_use to behave like use but fail if errors are detected. It can be used in all Makefiles except Pure, which will write the exception handler explicitly ("exit" will have been declared already).

Now the "use" call has an exception handler, for prompt failure if errors are detected.

Now calls exit_use instead of use, for prompt failure if errors are detected.

Removed an old bug which made some simultaneous instantiations fail if they were given in the "wrong" order. Rewrote sign/infer_types. Fixed some comments.

added exit 1

Removed superfluous type constraint

Changed treatment of during type inference internally generated type variables. 1. They are renamed to 'a, 'b, 'c etc away from a given set of used names. 2. They are either frozen (turned into TFrees) or left schematic (TVars) depending on a parameter. In goals they are frozen, for instantiations they are left schematic.

Added type constraints to enforce correct choice of variable names.

Put freeze into the signature TACTIC for export

Removed "localize"; instead, proofs refer to their own assumptions.

Commented isof(c,t)

Added dependencies on ../Provers/hypsubst.ML and removed those on ../Provers/ind.ML

Replaced read by read_cterm.

Enforced partial evaluation of mk_case_split_tac.

Enforced partial evaluation of mk_case_split_tac

Added dependencies on files in Provers

Added pretty-printing coments

*** empty log message ***

*** empty log message ***

Hoare logic

Changed Univ to Datatype in parents

Replaced rules by defs. Also got rid of tyconstU by including TyConst in the datatype's universe

Replaced rules by defs

Got rid of exvarU and constU by including ExVar and Const in various datatype universes.

Deleted constQU, exvarQU, expQU by including Const, ExpVar, Exp in Value.thy's codatatype declaration.

Replaced rules by defs