| Mon, 10 May 2010 13:58:18 +0200 | haftmann | less complex organization of cooper source code | changeset | files |
| Mon, 10 May 2010 12:25:49 +0200 | haftmann | dropped unused bindings; avoid open (documents dependency on generated code more explicitly) | changeset | files |
| Mon, 10 May 2010 14:53:33 -0700 | huffman | add real_mult_commute to legacy theorem names | changeset | files |
| Mon, 10 May 2010 12:12:58 -0700 | huffman | new construction of real numbers using Cauchy sequences | changeset | files |
| Mon, 10 May 2010 11:47:56 -0700 | huffman | add more credits to ex/Dedekind_Real.thy | changeset | files |
| Mon, 10 May 2010 11:30:05 -0700 | huffman | put construction of reals using Dedekind cuts in HOL/ex | changeset | files |