| Fri, 30 May 1997 15:21:53 +0200 | paulson | Addition of Finite as parent allows cardinality theorems | changeset | files |
| Fri, 30 May 1997 15:21:21 +0200 | paulson | Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs | changeset | files |
| Fri, 30 May 1997 15:20:41 +0200 | paulson | Overloading of "^" requires a type constraint | changeset | files |
| Fri, 30 May 1997 15:19:58 +0200 | paulson | Overloading of "^" requires new type class "power", with types "nat" and | changeset | files |
| Fri, 30 May 1997 15:17:36 +0200 | paulson | New theory Divides | changeset | files |
| Fri, 30 May 1997 15:17:14 +0200 | paulson | Many new theorems about cardinality | changeset | files |
| Fri, 30 May 1997 15:16:44 +0200 | paulson | Now Divides must be the parent | changeset | files |
| Fri, 30 May 1997 15:15:57 +0200 | paulson | Moving div and mod from Arith to Divides | changeset | files |