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