2001-11-19 ago wenzelm tuned;
2001-11-19 ago wenzelm multi_theorem: common statement header (covers *all* results);
2001-11-19 ago wenzelm fixed comment;
2001-11-19 ago wenzelm induct method: localize rews for rule;
2001-11-19 ago berghofe Now handles different theorems with same name more gracefully.
2001-11-19 ago berghofe Improved error message.
2001-11-19 ago berghofe Added setup.
2001-11-19 ago berghofe Moved fastype to Envir.
2001-11-19 ago berghofe Further restructuring of theorem naming functions.
2001-11-19 ago berghofe Added setup for proof rewrite rules.
2001-11-19 ago berghofe - Fixed bug in shrink
2001-11-19 ago berghofe Replaced devar by Envir.head_norm
2001-11-19 ago berghofe Moved head_norm and fastype from unify.ML to envir.ML
2001-11-16 ago kleing fixed maxs bug
2001-11-16 ago wenzelm Ntree and Brouwer converted and moved to ZF/Induct;
2001-11-16 ago wenzelm converted;
2001-11-16 ago wenzelm actually store "coinduct" rule;
2001-11-16 ago wenzelm additional P.marg_comment;
2001-11-16 ago wenzelm \usepackage[latin1]{inputenc};
2001-11-16 ago paulson even more theories from Jacques
2001-11-16 ago wenzelm finish_global: Drule.strip_shyps_warning (just for warning);
2001-11-16 ago wenzelm ext_tsig_classes: rebuild_tsig!!!!!
2001-11-16 ago wenzelm local_standard: plain strip_shyps instead of strip_shyps_warning;
2001-11-16 ago paulson last-minute tidying
2001-11-15 ago wenzelm updated;
2001-11-15 ago wenzelm GPLed;
2001-11-15 ago wenzelm write_keywords: string argument (logic name);
2001-11-15 ago wenzelm isatool unsymbolize;
2001-11-15 ago ehmety Modified to make the files build with the new changes in ZF
2001-11-15 ago wenzelm depends on Epsilon!
2001-11-15 ago wenzelm fix_frees: rev;
2001-11-15 ago wenzelm prove: raise ERROR_MESSAGE;
2001-11-15 ago wenzelm updated;
2001-11-15 ago wenzelm * ZF: new-style theory commands '(co)inductive', '(co)datatype',
2001-11-15 ago wenzelm type_solver_tac: use TCSET' to refer to context of goal state (does
2001-11-15 ago wenzelm setup DatatypeTactics.setup;
2001-11-15 ago wenzelm added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from
2001-11-15 ago wenzelm no handle ERROR;
2001-11-15 ago wenzelm fixed;
2001-11-15 ago wenzelm Isar version of 'rep_datatype';
2001-11-15 ago wenzelm avoid handle _;
2001-11-15 ago wenzelm added TCSET(') tacticals;
2001-11-15 ago wenzelm added Term and Tree_Forest (from converted ZF/ex);
2001-11-15 ago wenzelm TF and Term moved to ZF/Induct;
2001-11-15 ago paulson miniscoping of UN and INT
2001-11-15 ago ehmety Added new entry
2001-11-15 ago ehmety New files
2001-11-15 ago paulson new theories from Jacques Fleuriot
2001-11-15 ago ehmety *** empty log message ***
2001-11-14 ago wenzelm converted datatype examples moved from ZF/ex to ZF/Induct;
2001-11-14 ago wenzelm document setup;
2001-11-14 ago wenzelm removed BT, Data, Enum (see ZF/Induct);
2001-11-14 ago wenzelm case_names;
2001-11-14 ago wenzelm added Datatypes, Binary_Trees (from ZF/ex);
2001-11-14 ago wenzelm Isar attribute and method setup;
2001-11-14 ago wenzelm fix path prefix;
2001-11-14 ago wenzelm use proper intr_names (for required case_names);
2001-11-14 ago wenzelm added Induct/Binary_Trees.thy, Induct/Datatypes.thy;
2001-11-14 ago wenzelm tuned;
2001-11-14 ago wenzelm updated;