Replaced devar by Envir.head_norm

Moved head_norm and fastype from unify.ML to envir.ML

fixed maxs bug

Ntree and Brouwer converted and moved to ZF/Induct;

converted;

actually store "coinduct" rule;

additional P.marg_comment;

\usepackage[latin1]{inputenc};

even more theories from Jacques

finish_global: Drule.strip_shyps_warning (just for warning);

ext_tsig_classes: rebuild_tsig!!!!!

local_standard: plain strip_shyps instead of strip_shyps_warning;

last-minute tidying

updated;

GPLed;

write_keywords: string argument (logic name);

isatool unsymbolize;

Modified to make the files build with the new changes in ZF

depends on Epsilon!

fix_frees: rev;

prove: raise ERROR_MESSAGE;

updated;

* ZF: new-style theory commands '(co)inductive', '(co)datatype', 'rep_datatype', 'inductive_cases'; also methods 'ind_cases', 'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');

type_solver_tac: use TCSET' to refer to context of goal state (does *not* work with local proof contexts of Isar / new-style locales);

setup DatatypeTactics.setup;

added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from former ex/TF.ML ex/TF.thy ex/Term.ML ex/Term.thy);

no handle ERROR;

fixed;

Isar version of 'rep_datatype';

avoid handle _;

added TCSET(') tacticals;

added Term and Tree_Forest (from converted ZF/ex);