Wed, 20 Feb 2008 18:28:16 +0100 | huffman | fix proofs involving ile_def | changeset | files |
Wed, 20 Feb 2008 14:52:38 +0100 | haftmann | tuned structures in arith_data.ML | changeset | files |
Wed, 20 Feb 2008 14:52:34 +0100 | haftmann | using only an relation predicate to construct div and mod | changeset | files |