eliminated private clones of List.partition;

observe some Isabelle/ML coding conventions; avoid structure alias FT, which would complicate systematic searches unnecessarily;

eliminated NJ's List.nth;

tuned CHANGED_GOAL: use Thm.cprem_of instead of selecting from Thm.prems_of;

tuned/unified size_of_term and size_of_typ, eliminated obsolete foldl;

observe basic Isabelle/ML coding conventions;

moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;

added ML-Systems/polyml-experimental.ML; more systematic treatment of bootstrap files;

tuned;

even less default memory for sunbroy2;

merged

merged

Made then_conv and else_conv available as infix operations.

merged

fixed typo

merged

avoid using legacy type inference

use TheoryData to keep track of pattern match combinators

merged

remove unnecessary simp rules

revert some Suc 0 lemmas back to their original forms; added some simp rules for (1::nat)

merged

back to canonical ROOT, to see if memory problems still persist;

trying less default memory for sunbroy2 test

basic setup for chapter "Syntax and type-checking";

merged

standard headers; eliminated non-ASCII chars, which are fragile in the age of unicode;

updated generated files;

uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities; more robust handling of "|" within index;

fixed import of ~~/src/HOL/Decision_Procs/Ferrack;