| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Wed, 03 Oct 2001 20:54:16 +0200 |
wenzelm |
tuned parentheses in relational expressions;
|
file |
diff |
annotate
|
| Mon, 06 Aug 2001 13:43:24 +0200 |
nipkow |
turned translation for 1::nat into def.
|
file |
diff |
annotate
|
| Tue, 09 Jan 2001 15:32:27 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 05 Jan 2001 18:48:18 +0100 |
nipkow |
^^ -> ```
|
file |
diff |
annotate
|
| Tue, 12 Dec 2000 11:59:25 +0100 |
paulson |
deleting unused rules
|
file |
diff |
annotate
|
| Fri, 01 Dec 2000 11:02:55 +0100 |
paulson |
renamed less_eq_Suc_add to less_imp_Suc_add
|
file |
diff |
annotate
|
| Mon, 27 Nov 2000 11:06:28 +0100 |
paulson |
deleted unused result intrel_refl
|
file |
diff |
annotate
|
| Wed, 15 Nov 2000 19:42:58 +0100 |
wenzelm |
renamed integ_le_less to int_le_less;
|
file |
diff |
annotate
|
| Fri, 10 Nov 2000 19:18:37 +0100 |
wenzelm |
int_distrib;
|
file |
diff |
annotate
|
| Mon, 07 Aug 2000 10:27:11 +0200 |
paulson |
added a dummy "thm list" argument to prove_conv for the new interface to
|
file |
diff |
annotate
|
| Wed, 19 Jul 2000 12:33:36 +0200 |
paulson |
changed / to // for quotienting
|
file |
diff |
annotate
|
| Sun, 16 Jul 2000 20:56:14 +0200 |
wenzelm |
use pair_tac;
|
file |
diff |
annotate
|
| Thu, 22 Jun 2000 23:04:34 +0200 |
wenzelm |
bind_thm(s);
|
file |
diff |
annotate
|
| Wed, 24 May 2000 18:41:09 +0200 |
paulson |
installing plus_ac0 for int
|
file |
diff |
annotate
|
| Tue, 23 May 2000 18:14:57 +0200 |
paulson |
defining 0::int to be (int 0)
|
file |
diff |
annotate
|
| Wed, 01 Sep 1999 21:25:55 +0200 |
wenzelm |
bind_thms;
|
file |
diff |
annotate
|
| Fri, 27 Aug 1999 15:42:10 +0200 |
paulson |
tidied, allowing pattern-matching in defs of zadd and zmult
|
file |
diff |
annotate
|
| Thu, 29 Jul 1999 12:44:57 +0200 |
paulson |
added parentheses to cope with a possible reduction of the precedence of unary
|
file |
diff |
annotate
|
| Thu, 15 Jul 1999 10:34:37 +0200 |
paulson |
more renaming of theorems from _nat to _int (corresponding to a function that
|
file |
diff |
annotate
|
| Tue, 13 Jul 1999 10:44:45 +0200 |
paulson |
renamed inj_nat to inj_int
|
file |
diff |
annotate
|
| Thu, 08 Jul 1999 13:43:42 +0200 |
paulson |
Introduction of integer division algorithm
|
file |
diff |
annotate
|
| Wed, 23 Jun 1999 10:37:29 +0200 |
paulson |
new distributive laws involving * and -
|
file |
diff |
annotate
|
| Mon, 24 May 1999 15:54:58 +0200 |
paulson |
int_Suc->int_Suc_int_1 avoiding confusion with the more useful Bin.int_Suc
|
file |
diff |
annotate
|
| Fri, 21 May 1999 10:47:07 +0200 |
paulson |
deleted some vestigal theorems (use the equivalents on HOL/Ord.ML)
|
file |
diff |
annotate
|
| Wed, 13 Jan 1999 12:16:34 +0100 |
nipkow |
Refined arithmetic.
|
file |
diff |
annotate
|
| Mon, 11 Jan 1999 16:50:49 +0100 |
nipkow |
More arith simplifications.
|
file |
diff |
annotate
|
| Fri, 27 Nov 1998 17:00:30 +0100 |
nipkow |
At last: linear arithmetic for nat!
|
file |
diff |
annotate
|
| Fri, 23 Oct 1998 20:44:34 +0200 |
oheimb |
corrected auto_tac (applications of unsafe wrappers)
|
file |
diff |
annotate
|
| Thu, 01 Oct 1998 18:27:17 +0200 |
paulson |
much tidying
|
file |
diff |
annotate
|
| Tue, 29 Sep 1998 15:57:42 +0200 |
paulson |
many renamings and changes. Simproc for cancelling common terms in relations
|
file |
diff |
annotate
|
| Fri, 25 Sep 1998 13:57:01 +0200 |
paulson |
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
|
file |
diff |
annotate
|
| Wed, 23 Sep 1998 10:25:37 +0200 |
paulson |
much renaming and reorganization
|
file |
diff |
annotate
|
| Fri, 18 Sep 1998 16:04:00 +0200 |
paulson |
new files in Integ
|
file |
diff |
annotate
|