Thu, 08 Jul 1999 18:34:59 +0200 |
wenzelm |
propp: 'concl' patterns;
|
changeset |
files
|
Thu, 08 Jul 1999 18:32:43 +0200 |
wenzelm |
propp: 'concl' patterns;
|
changeset |
files
|
Thu, 08 Jul 1999 18:31:04 +0200 |
wenzelm |
improved error msgs of cterm_instantiate;
|
changeset |
files
|
Thu, 08 Jul 1999 18:30:21 +0200 |
wenzelm |
aprop: ??id, ...;
|
changeset |
files
|
Thu, 08 Jul 1999 18:30:00 +0200 |
wenzelm |
improved error msgs of instantiate;
|
changeset |
files
|
Thu, 08 Jul 1999 18:29:30 +0200 |
wenzelm |
added commute: 'a seq list -> 'a list seq;
|
changeset |
files
|
Thu, 08 Jul 1999 18:29:07 +0200 |
wenzelm |
added pretty_thm_no_hyps;
|
changeset |
files
|
Thu, 08 Jul 1999 18:28:02 +0200 |
wenzelm |
theorems involving oracles are now printed with a suffixed [!];
|
changeset |
files
|
Thu, 08 Jul 1999 18:27:01 +0200 |
wenzelm |
Theorems involving oracles will be printed with a suffixed \verb|[!]|;
|
changeset |
files
|
Thu, 08 Jul 1999 18:26:24 +0200 |
wenzelm |
updated usedir;
|
changeset |
files
|
Thu, 08 Jul 1999 13:55:18 +0200 |
paulson |
integer division
|
changeset |
files
|
Thu, 08 Jul 1999 13:48:11 +0200 |
paulson |
Renaming of theorems from _nat0 to _int0 and _nat1 to _int1
|
changeset |
files
|
Thu, 08 Jul 1999 13:47:27 +0200 |
paulson |
Introduction of integer division algorithm
|
changeset |
files
|
Thu, 08 Jul 1999 13:46:29 +0200 |
paulson |
changed header to cope with default if_weak_cong
|
changeset |
files
|
Thu, 08 Jul 1999 13:44:47 +0200 |
paulson |
Now if_weak_cong is a standard congruence rule
|
changeset |
files
|
Thu, 08 Jul 1999 13:43:42 +0200 |
paulson |
Introduction of integer division algorithm
|
changeset |
files
|