| Tue, 20 May 2014 19:24:39 +0200 | hoelzl | add various lemmas | file | diff | annotate |
| Mon, 19 May 2014 12:04:45 +0200 | hoelzl | introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces | file | diff | annotate |
| Tue, 11 Mar 2014 11:32:32 +0100 | hoelzl | measurable_lfp/gfp: indirection not necessary | file | diff | annotate |
| Mon, 10 Mar 2014 20:16:13 +0100 | hoelzl | add measurability rule for (co)inductive predicates | file | diff | annotate |
| Fri, 16 Aug 2013 21:33:36 +0200 | wenzelm | more standard attribute_setup / method_setup -- export key ML operations instead of parsers; | file | diff | annotate |
| Fri, 14 Dec 2012 16:33:22 +0100 | wenzelm | updated some headers; | file | diff | annotate |
| Wed, 05 Dec 2012 15:59:08 +0100 | hoelzl | Move the measurability prover to its own file | file | diff | annotate |