| Mon, 13 Mar 2000 16:23:34 +0100 |
wenzelm |
case_tac now subsumes both boolean and datatype cases;
|
file |
diff |
annotate
|
| Mon, 13 Mar 2000 12:51:10 +0100 |
nipkow |
exhaust_tac -> cases_tac
|
file |
diff |
annotate
|
| Mon, 19 Jul 1999 15:32:14 +0200 |
paulson |
examples of arithmetic on the naturals
|
file |
diff |
annotate
|
| Thu, 08 Jul 1999 13:47:27 +0200 |
paulson |
Introduction of integer division algorithm
|
file |
diff |
annotate
|
| Tue, 06 Jul 1999 21:13:12 +0200 |
wenzelm |
adapted to generic numerals;
|
file |
diff |
annotate
|
| Fri, 23 Oct 1998 18:47:44 +0200 |
paulson |
Now users will never see (int 0)
|
file |
diff |
annotate
|
| Thu, 01 Oct 1998 18:30:05 +0200 |
paulson |
revised for new treatment of integers
|
file |
diff |
annotate
|
| Fri, 25 Sep 1998 14:06:56 +0200 |
paulson |
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
|
file |
diff |
annotate
|
| Thu, 24 Sep 1998 15:20:29 +0200 |
paulson |
added correctness proofs for arithmetic
|
file |
diff |
annotate
|
| Mon, 21 Sep 1998 10:43:54 +0200 |
paulson |
Unary minus is now #- and not #~
|
file |
diff |
annotate
|
| Tue, 15 Sep 1998 15:06:29 +0200 |
paulson |
revised treatment of integers
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 17:55:57 +0200 |
wenzelm |
added ex/MonoidGroups (record example);
|
file |
diff |
annotate
|