1998-10-21 berghofe 1998-10-21 Changed syntax of rep_datatype and inductive: Theorems are no longer specified by a string of ML type "thm list" but by a comma-separated list of identifiers, which are looked up in the theory.
1998-10-21 berghofe 1998-10-21 Added theorem prod_induct (needed for rep_datatype).
1998-10-21 berghofe 1998-10-21 Changed syntax of rep_datatype.
1998-10-21 wenzelm 1998-10-21 fixed field_injects;
1998-10-21 wenzelm 1998-10-21 tuned;
1998-10-21 wenzelm 1998-10-21 no open;
1998-10-21 wenzelm 1998-10-21 tuned;
1998-10-21 nipkow 1998-10-21 Tutorial
1998-10-21 wenzelm 1998-10-21 dropped support for SML/NJ 109.x;
1998-10-21 wenzelm 1998-10-21 field_injects [iffs];
1998-10-21 wenzelm 1998-10-21 record_split_name;
1998-10-21 wenzelm 1998-10-21 tuned (all proofs are INSTABLE by David's definition of instability);
1998-10-21 wenzelm 1998-10-21 improved var names; tuned;
1998-10-20 wenzelm 1998-10-20 tuned stack_overflow_handler;
1998-10-20 wenzelm 1998-10-20 made SML/NJ happy;
1998-10-20 wenzelm 1998-10-20 delSWrapper "record_split_tac";
1998-10-20 wenzelm 1998-10-20 fixed Syntax module;
1998-10-20 wenzelm 1998-10-20 split_paired_all.ML;
1998-10-20 wenzelm 1998-10-20 field types: datatype; record_split_tac; quiet_mode; renamed fst/snd to val/more; structure BasicRecordPackage;
1998-10-20 wenzelm 1998-10-20 quiet_mode, message;
1998-10-20 wenzelm 1998-10-20 quiet proofs;
1998-10-20 wenzelm 1998-10-20 fixed Syntax module;
1998-10-20 wenzelm 1998-10-20 Datatype instead of Prod;
1998-10-20 wenzelm 1998-10-20 QUIET_BREADTH_FIRST;
1998-10-20 wenzelm 1998-10-20 no open; handle multiple trfuns; tuned; removed trfun_names; structure BasicSyntax;
1998-10-20 wenzelm 1998-10-20 no open; handle multiple trfuns;
1998-10-20 wenzelm 1998-10-20 no open;
1998-10-20 wenzelm 1998-10-20 simple Env replaced by Symtab;
1998-10-20 wenzelm 1998-10-20 added unvarify(T);
1998-10-20 wenzelm 1998-10-20 Syntax.max_pri;
1998-10-20 wenzelm 1998-10-20 Symtab.foldl;
1998-10-20 wenzelm 1998-10-20 quiet_mode, message;
1998-10-20 wenzelm 1998-10-20 structure Hidden = struct end;
1998-10-20 wenzelm 1998-10-20 hiding private stuff;
1998-10-20 wenzelm 1998-10-20 Symtab.foldl;
1998-10-20 wenzelm 1998-10-20 added foldl, keys;
1998-10-20 wenzelm 1998-10-20 split_paired_all.ML: turn surjective pairing into split rule;
1998-10-20 paulson 1998-10-20 updated
1998-10-20 paulson 1998-10-20 updated the MLWorks description
1998-10-19 mueller 1998-10-19 another little bug ;-) and minor changes in TLS.*;
1998-10-19 mueller 1998-10-19 little bug ;-)
1998-10-19 oheimb 1998-10-19 added keyword 'and'
1998-10-19 oheimb 1998-10-19 corrected Header
1998-10-19 nipkow 1998-10-19 Addsimps [max_le_iff_conj]; Addsimps [le_min_iff_conj];
1998-10-19 oheimb 1998-10-19 changed Super_L and Hyper_R to left and right Meta
1998-10-19 oheimb 1998-10-19 layout
1998-10-19 mueller 1998-10-19 solved conflict by taking newest version;
1998-10-19 paulson 1998-10-19 added Clarify_tac to speed up proofs
1998-10-19 paulson 1998-10-19 moved a theorem
1998-10-19 paulson 1998-10-19 fixed comment
1998-10-19 paulson 1998-10-19 fixed some indenting; changed a VERY slow blast_tac to fast_tac
1998-10-18 wenzelm 1998-10-18 updated, tuned;
1998-10-18 wenzelm 1998-10-18 added Minho (Portugal);
1998-10-16 berghofe 1998-10-16 Fixed bug (improper handling of flag flat_names).
1998-10-16 berghofe 1998-10-16 Added quiet_mode flag.
1998-10-16 berghofe 1998-10-16 - Changed structure of name spaces - Proofs for datatypes with unneeded parameters are working now - added additional parameter flat_names - added quiet_mode flag
1998-10-16 wenzelm 1998-10-16 tuned MLWorks options; added print_depth;
1998-10-16 wenzelm 1998-10-16 MLWorks 2.0;
1998-10-16 berghofe 1998-10-16 Changed structure of name spaces for datatypes.
1998-10-16 nipkow 1998-10-16 2. The simplifier now knows a little bit about nat-arithmetic.