deleted a reference to "nat", now erroneous because "nat" is a function

many new laws about div and mod

new theorem zless_zero_nat

removal of rewrites for Suc(Suc(Suc...)))

NatBin: binary arithmetic for the naturals

getting rid of qed_goal

getting rid of qed_goal

new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m

Modifid length_tl

adapted to dest_keywords, dest_parsers;

separate command tokens;

tuned dest_lexicon;

tuned;

removed break;

removed BREAK, ROLLBACK;

structure LocalDefs = LocalDefs; structure Calculation = Calculation; structure SkipProof = SkipProof;

Exported function unify_consts (workaround to avoid inconsistently typed recursive constants in inductive and primrec definitions).

Added new example (infinitely branching trees).

Infinitely branching trees.

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).

- 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

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

qed_goal -> Goal

tuned;

tuned comments;