summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

Replaced datatype_info by datatype_info_err.

- Now also supports arbitrarily branching datatypes.
- Fixed bug (in some rare cases, recursive constants were
inconsistently typed in different primrec equations).

Fri, 16 Jul 1999 12:14:04 +0200
- Datatype package now also supports arbitrarily branching datatypes

- Datatype package now also supports arbitrarily branching datatypes
(using function types).
- Added new simplification procedure for proving distinctness of
constructors.
- dtK is now a reference.

Added some definitions and theorems needed for the
construction of datatypes involving function types.

Some rather large datatype examples (from John Harrison).

improved print_thms;

export init_state;
end_proof: reset goal_facts;

more renaming of theorems from _nat to _int (corresponding to a function that
was similarly renamed some time ago
Also new theorem zmult_int

more renaming of theorems from _nat to _int (corresponding to a function that
was similarly renamed some time ago

Thu, 15 Jul 1999 10:33:16 +0200
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int

qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int