| 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
|
| Thu, 08 Jul 1999 13:42:31 +0200 |
paulson |
tidied proofs to cope with default if_weak_cong
|
changeset |
files
|
| Thu, 08 Jul 1999 13:38:41 +0200 |
paulson |
Now if_weak_cong is a standard congruence rule
|
changeset |
files
|
| Thu, 08 Jul 1999 13:37:40 +0200 |
paulson |
new theory IntDiv.thy
|
changeset |
files
|
| Thu, 08 Jul 1999 13:35:33 +0200 |
paulson |
new files IntDiv.{thy,ML}
|
changeset |
files
|
| Wed, 07 Jul 1999 00:15:06 +0200 |
wenzelm |
tuned output;
|
changeset |
files
|
| Tue, 06 Jul 1999 21:16:29 +0200 |
wenzelm |
simp only: attribute, method arg;
|
changeset |
files
|
| Tue, 06 Jul 1999 21:14:34 +0200 |
wenzelm |
use generic numeral encoding and syntax;
|
changeset |
files
|
| Tue, 06 Jul 1999 21:13:12 +0200 |
wenzelm |
adapted to generic numerals;
|
changeset |
files
|
| Tue, 06 Jul 1999 21:11:34 +0200 |
wenzelm |
simp only;
|
changeset |
files
|
| Tue, 06 Jul 1999 21:09:23 +0200 |
wenzelm |
added Numeral.thy;
|
changeset |
files
|
| Tue, 06 Jul 1999 21:09:05 +0200 |
wenzelm |
_reflcl;
|
changeset |
files
|
| Tue, 06 Jul 1999 21:08:30 +0200 |
wenzelm |
added Numeral.thy, Tools/numeral_syntax.ML;
|
changeset |
files
|
| Tue, 06 Jul 1999 21:06:51 +0200 |
wenzelm |
removed proof history nesting commands (not useful);
|
changeset |
files
|
| Tue, 06 Jul 1999 21:06:03 +0200 |
wenzelm |
improved errors;
|
changeset |
files
|
| Tue, 06 Jul 1999 21:04:37 +0200 |
wenzelm |
removed nesting (unused);
|
changeset |
files
|
| Tue, 06 Jul 1999 21:03:57 +0200 |
wenzelm |
export term_of_typ;
|
changeset |
files
|