| Thu, 22 Apr 2004 10:43:06 +0200 | 
paulson | 
new lemmas
 | 
file |
diff |
annotate
 | 
| Fri, 05 Mar 2004 15:26:04 +0100 | 
paulson | 
some new results
 | 
file |
diff |
annotate
 | 
| Thu, 04 Mar 2004 12:06:07 +0100 | 
paulson | 
new material from Avigad, and simplified treatment of division by 0
 | 
file |
diff |
annotate
 | 
| Tue, 25 Nov 2003 10:37:03 +0100 | 
paulson | 
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
 | 
file |
diff |
annotate
 | 
| Fri, 26 Sep 2003 10:34:57 +0200 | 
paulson | 
misc tidying
 | 
file |
diff |
annotate
 | 
| Thu, 24 Jul 2003 18:23:00 +0200 | 
paulson | 
declarations moved from PreList.thy
 | 
file |
diff |
annotate
 | 
| Tue, 25 Mar 2003 09:56:01 +0100 | 
berghofe | 
New theorems split_div' and mod_div_equality'.
 | 
file |
diff |
annotate
 | 
| Fri, 23 Aug 2002 07:41:05 +0200 | 
nipkow | 
Added div+mod cancelling simproc
 | 
file |
diff |
annotate
 | 
| Fri, 31 May 2002 07:53:37 +0200 | 
nipkow | 
Now arith can deal with div/mod arbitrary nat numerals.
 | 
file |
diff |
annotate
 | 
| Wed, 15 May 2002 13:49:51 +0200 | 
nipkow | 
Divides.ML -> Divides_lemmas.ML
 | 
file |
diff |
annotate
 | 
| Sat, 01 Dec 2001 18:52:32 +0100 | 
wenzelm | 
renamed class "term" to "type" (actually "HOL.type");
 | 
file |
diff |
annotate
 | 
| Fri, 05 Jan 2001 14:28:10 +0100 | 
nipkow | 
Changed priority of dvd from 70 to 50 as befits a relation.
 | 
file |
diff |
annotate
 | 
| Fri, 01 Dec 2000 11:03:31 +0100 | 
paulson | 
many new div and mod properties (borrowed from Integ/IntDiv)
 | 
file |
diff |
annotate
 | 
| Fri, 13 Oct 2000 08:28:21 +0200 | 
nipkow | 
*** empty log message ***
 | 
file |
diff |
annotate
 | 
| Thu, 12 Oct 2000 18:38:23 +0200 | 
nipkow | 
*** empty log message ***
 | 
file |
diff |
annotate
 | 
| Wed, 24 May 2000 18:48:22 +0200 | 
paulson | 
installing plus_ac0 for nat
 | 
file |
diff |
annotate
 | 
| Sun, 21 May 2000 14:49:28 +0200 | 
wenzelm | 
replaced {{ }} by { };
 | 
file |
diff |
annotate
 | 
| Mon, 19 Jul 1999 15:18:16 +0200 | 
paulson | 
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
 | 
file |
diff |
annotate
 | 
| Thu, 01 Jul 1999 10:33:50 +0200 | 
paulson | 
now div and mod are overloaded; dvd is polymorphic
 | 
file |
diff |
annotate
 | 
| Fri, 30 May 1997 15:15:57 +0200 | 
paulson | 
Moving div and mod from Arith to Divides
 | 
file |
diff |
annotate
 |