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

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

qed_goal -> Goal

tuned;

tuned comments;