| Tue, 02 Jun 2009 15:53:05 +0200 | haftmann | OCaml builtin intergers are elusive; avoid | changeset | files |
| Tue, 02 Jun 2009 15:53:04 +0200 | haftmann | more aggresive bracketing of let expressions | changeset | files |
| Tue, 02 Jun 2009 15:53:03 +0200 | haftmann | tuned whitespace | changeset | files |
| Tue, 02 Jun 2009 16:56:55 +0200 | wenzelm | merged | changeset | files |
| Tue, 02 Jun 2009 16:10:51 +0200 | wenzelm | merged | changeset | files |
| Tue, 02 Jun 2009 15:06:17 +0200 | chaieb | merged | changeset | files |
| Tue, 02 Jun 2009 12:18:44 +0200 | chaieb | merged | changeset | files |
| Tue, 02 Jun 2009 12:18:08 +0200 | chaieb | merged | changeset | files |
| Mon, 01 Jun 2009 09:26:28 +0200 | chaieb | Reverses idempotent; radical of E; generalized logarithm; | changeset | files |
| Tue, 02 Jun 2009 16:52:37 +0200 | wenzelm | made SML/NJ happy; | changeset | files |
| Tue, 02 Jun 2009 14:43:47 +0200 | wenzelm | merged | changeset | files |
| Tue, 02 Jun 2009 14:37:05 +0200 | hoelzl | use algebra_simps instead of ring_simps | changeset | files |
| Tue, 02 Jun 2009 14:38:10 +0200 | wenzelm | merged, resolving conflict in src/Pure/Isar/attrib.ML; | changeset | files |
| Tue, 02 Jun 2009 14:00:24 +0200 | hoelzl | Generalized Integral_add | changeset | files |
| Tue, 02 Jun 2009 13:59:32 +0200 | hoelzl | Added theorems about distinct & concat, map & replicate and concat & replicate | changeset | files |
| Tue, 02 Jun 2009 10:04:03 +0200 | berghofe | merged | changeset | files |
| Tue, 02 Jun 2009 10:02:52 +0200 | berghofe | Fixed broken code dealing with alternative names. | changeset | files |
| Tue, 02 Jun 2009 10:02:08 +0200 | berghofe | Enclosed parts of subsection in @{text ...} to make LaTeX happy. | changeset | files |
| Tue, 02 Jun 2009 10:00:29 +0200 | berghofe | Added Convex_Euclidean_Space.thy again. | changeset | files |
| Tue, 02 Jun 2009 08:56:19 +0200 | haftmann | made SML/NJ happy | changeset | files |
| Mon, 01 Jun 2009 16:27:54 -0700 | huffman | declare Bfun_def [code del] | changeset | files |
| Mon, 01 Jun 2009 10:56:31 -0700 | huffman | simp del -> code del | changeset | files |
| Mon, 01 Jun 2009 10:36:42 -0700 | huffman | limits of inverse using filters | changeset | files |
| Mon, 01 Jun 2009 08:04:19 -0700 | huffman | merged | changeset | files |
| Mon, 01 Jun 2009 07:57:37 -0700 | huffman | add [code del] declarations | changeset | files |
| Mon, 01 Jun 2009 07:45:49 -0700 | huffman | add dependency on Limits.thy | changeset | files |
| Mon, 01 Jun 2009 10:02:01 +0200 | nipkow | new lemma | changeset | files |
| Sun, 31 May 2009 22:00:56 -0700 | huffman | merged | changeset | files |
| Sun, 31 May 2009 21:59:33 -0700 | huffman | new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters | changeset | files |
| Sun, 31 May 2009 11:27:19 -0700 | huffman | more abstract properties of eventually | changeset | files |