1998-10-23 berghofe New example for using the datatype package:
1998-10-23 berghofe Removed obsolete theory Simult (see theory Term).
1998-10-23 wenzelm started to add records;
1998-10-23 paulson occurs check now handles Bound variables (for soundness)
1998-10-23 wenzelm updated by isatool logo;
1998-10-22 wenzelm tuned block indent;
1998-10-22 wenzelm current_goals_markers;
1998-10-22 wenzelm some additions for Proof General by David Aspinall;
1998-10-22 wenzelm support current_goals_markers ref variable for print_current_goals;
1998-10-22 wenzelm eliminated 'let ... in structure ...' to make SML/NJ 0.93 happy;
1998-10-22 wenzelm fixed index.html;
1998-10-22 wenzelm tuned;
1998-10-22 wenzelm tuned;
1998-10-22 paulson standard Blast_tac demos
1998-10-22 paulson tidying
1998-10-22 paulson locales
1998-10-21 berghofe Changed interface of inductive.
1998-10-21 berghofe Changed interface of rep_datatype: Characteristic theorems
1998-10-21 berghofe Changed interface.
1998-10-21 berghofe Changed interface of add_inductive: monos and con_defs are now
1998-10-21 berghofe Changed syntax of inductive.
1998-10-21 berghofe Changed syntax of rep_datatype and inductive: Theorems
1998-10-21 berghofe Added theorem prod_induct (needed for rep_datatype).
1998-10-21 berghofe Changed syntax of rep_datatype.
1998-10-21 wenzelm fixed field_injects;
1998-10-21 wenzelm tuned;
1998-10-21 wenzelm no open;
1998-10-21 wenzelm tuned;
1998-10-21 nipkow Tutorial
1998-10-21 wenzelm dropped support for SML/NJ 109.x;
1998-10-21 wenzelm field_injects [iffs];
1998-10-21 wenzelm record_split_name;
1998-10-21 wenzelm tuned (all proofs are INSTABLE by David's definition of instability);
1998-10-21 wenzelm improved var names;
1998-10-20 wenzelm tuned stack_overflow_handler;
1998-10-20 wenzelm made SML/NJ happy;
1998-10-20 wenzelm delSWrapper "record_split_tac";
1998-10-20 wenzelm fixed Syntax module;
1998-10-20 wenzelm split_paired_all.ML;
1998-10-20 wenzelm field types: datatype;
1998-10-20 wenzelm quiet_mode, message;
1998-10-20 wenzelm quiet proofs;
1998-10-20 wenzelm fixed Syntax module;
1998-10-20 wenzelm Datatype instead of Prod;
1998-10-20 wenzelm QUIET_BREADTH_FIRST;
1998-10-20 wenzelm no open;
1998-10-20 wenzelm no open;
1998-10-20 wenzelm no open;
1998-10-20 wenzelm simple Env replaced by Symtab;
1998-10-20 wenzelm added unvarify(T);
1998-10-20 wenzelm Syntax.max_pri;
1998-10-20 wenzelm Symtab.foldl;
1998-10-20 wenzelm quiet_mode, message;
1998-10-20 wenzelm structure Hidden = struct end;
1998-10-20 wenzelm hiding private stuff;
1998-10-20 wenzelm Symtab.foldl;
1998-10-20 wenzelm added foldl, keys;
1998-10-20 wenzelm split_paired_all.ML: turn surjective pairing into split rule;
1998-10-20 paulson updated
1998-10-20 paulson updated the MLWorks description
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip