| Mon, 17 Oct 2005 23:10:23 +0200 |
wenzelm |
added pos/negDivAlg_induct declarations (from Main.thy);
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
| Tue, 01 Oct 2002 13:26:10 +0200 |
paulson |
Numerous cosmetic changes, prompted by the new simplifier
|
file |
diff |
annotate
|
| Mon, 30 Sep 2002 16:48:15 +0200 |
berghofe |
Adapted to new simplifier.
|
file |
diff |
annotate
|
| Sat, 07 Sep 2002 22:04:28 +0200 |
paulson |
conversion of ZF/Integ/{Int,Bin} to Isar scripts
|
file |
diff |
annotate
|
| Tue, 27 Aug 2002 15:40:33 +0200 |
wenzelm |
avoid duplicate fact bindings;
|
file |
diff |
annotate
|
| Sat, 24 Aug 2002 18:45:21 +0200 |
paulson |
conversion of ZF/IntDiv to Isar script
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 12:11:00 +0200 |
paulson |
deleted the redundant first argument of adjust(a,b)
|
file |
diff |
annotate
|
| Mon, 21 May 2001 14:52:27 +0200 |
paulson |
the rest of integer division
|
file |
diff |
annotate
|
| Thu, 14 Sep 2000 11:34:13 +0200 |
paulson |
a bit more of division
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 17:36:37 +0200 |
paulson |
a number of new theorems
|
file |
diff |
annotate
|
| Fri, 11 Aug 2000 13:27:17 +0200 |
paulson |
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
|
file |
diff |
annotate
|