Wed, 16 Nov 2011 20:56:21 +0100 wenzelm tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
Wed, 16 Nov 2011 17:59:58 +0100 blanchet compile
Wed, 16 Nov 2011 17:26:42 +0100 blanchet compile
Wed, 16 Nov 2011 17:19:08 +0100 blanchet compile
Wed, 16 Nov 2011 17:06:14 +0100 blanchet give each time slice its own lambda translation
Wed, 16 Nov 2011 16:35:19 +0100 blanchet thread in additional options to minimizer
Wed, 16 Nov 2011 13:22:36 +0100 blanchet make metis reconstruction handling more flexible
Wed, 16 Nov 2011 11:16:23 +0100 blanchet document metis options better
Wed, 16 Nov 2011 10:44:36 +0100 blanchet fixed typo
Wed, 16 Nov 2011 10:34:08 +0100 blanchet document "lam_trans" option
Wed, 16 Nov 2011 10:09:44 +0100 blanchet nicer bullets
Wed, 16 Nov 2011 09:42:27 +0100 blanchet parse lambda translation option in Metis
Tue, 15 Nov 2011 22:20:58 +0100 blanchet rename the lambda translation schemes, so that they are understandable out of context
Tue, 15 Nov 2011 22:15:51 +0100 blanchet rename configuration option to more reasonable length
Tue, 15 Nov 2011 22:13:39 +0100 blanchet continued implementation of lambda-lifting in Metis
Tue, 15 Nov 2011 22:13:39 +0100 blanchet disable debugging output
Tue, 15 Nov 2011 22:13:39 +0100 blanchet use consts, not frees, for lambda-lifting
Tue, 15 Nov 2011 22:13:39 +0100 blanchet started implementing lambda-lifting in Metis
Tue, 15 Nov 2011 15:38:50 +0100 bulwahn improved generators for rational numbers to generate negative numbers;
Tue, 15 Nov 2011 15:38:49 +0100 bulwahn tuned
Tue, 15 Nov 2011 12:51:14 +0100 huffman remove one more old-style semicolon
Tue, 15 Nov 2011 12:49:05 +0100 huffman Metis_Examples/Big_O.thy: add number_ring class constraints, adapt proofs to use cancellation simprocs
Tue, 15 Nov 2011 12:39:49 +0100 huffman remove old-style semicolons
Tue, 15 Nov 2011 12:39:29 +0100 huffman avoid theorem references like 'semiring_norm(111)'
Tue, 15 Nov 2011 09:22:19 +0100 huffman merged
Mon, 14 Nov 2011 19:35:41 +0100 huffman merged
Mon, 14 Nov 2011 19:35:05 +0100 huffman Parametric_Ferrante_Rackoff.thy: restrict to class number_ring, replace '1+1' with '2' everywhere
Mon, 14 Nov 2011 09:49:05 +0100 huffman avoid numeral-representation-specific rules in metis proof
Mon, 14 Nov 2011 23:13:23 +0100 wenzelm merged
Mon, 14 Nov 2011 21:11:31 +0100 hoelzl remove sorry, otherwise it breaks the testboard
Mon, 14 Nov 2011 18:36:31 +0100 hoelzl cleaned up float theories; removed duplicate definitions and theorems
Mon, 14 Nov 2011 12:28:34 +0100 hoelzl enforce quick_and_dirty in Code_Real_Approx_By_Float
Mon, 14 Nov 2011 23:00:56 +0100 wenzelm some support for partial evaluation of attributed facts;
Mon, 14 Nov 2011 20:25:22 +0100 wenzelm tuned;
Mon, 14 Nov 2011 19:27:42 +0100 wenzelm eliminated dead code;
Mon, 14 Nov 2011 17:48:26 +0100 wenzelm inner syntax positions for string literals;
Mon, 14 Nov 2011 17:47:59 +0100 wenzelm less confusion subexpression markup;
Mon, 14 Nov 2011 16:52:19 +0100 wenzelm pass positions for named targets, for formal links in the document model;
Mon, 14 Nov 2011 16:24:50 +0100 wenzelm simplified Runtime.exn_messages: always print detailed version of low-level exeptions, which should not occur in regular user errors anyway;
Mon, 14 Nov 2011 16:16:49 +0100 wenzelm more detailed exception_trace: in Poly/ML 5.4.x intermediate handlers reset the trace (cf. Poly/ML SVN 1110);
Mon, 14 Nov 2011 12:29:19 +0100 bulwahn merged
Mon, 14 Nov 2011 11:14:06 +0100 bulwahn setting up exhaustive generators which are used for the smart generators
Mon, 14 Nov 2011 11:50:52 +0100 hoelzl add Code_Real_Approx_By_Float
Mon, 14 Nov 2011 09:25:05 +0100 huffman merged
Sun, 13 Nov 2011 19:30:35 +0100 huffman remove lemma float_remove_real_numeral, which duplicated Float.float_number_of
Sun, 13 Nov 2011 19:26:53 +0100 huffman remove unnecessary number-representation-specific rules from metis calls;
Sun, 13 Nov 2011 20:28:22 +0100 blanchet avoid confusing selector output
Sun, 13 Nov 2011 20:28:22 +0100 blanchet remove unsound line in Nitpick's "rat" setup
Sat, 12 Nov 2011 21:10:56 +0100 wenzelm tuned proofs;
Sat, 12 Nov 2011 20:14:09 +0100 wenzelm merged
Sat, 12 Nov 2011 13:01:56 +0100 huffman removed some old-style semicolons
Sat, 12 Nov 2011 19:44:56 +0100 wenzelm index markup elements for more efficient cumulate/select operations;
Sat, 12 Nov 2011 18:56:49 +0100 wenzelm tuned;
Sat, 12 Nov 2011 18:05:31 +0100 wenzelm tuned markup -- prefer user-perspective;
Sat, 12 Nov 2011 17:53:48 +0100 wenzelm tuned specifications and proofs;
Sat, 12 Nov 2011 17:52:28 +0100 wenzelm more precise type;
Sat, 12 Nov 2011 17:01:58 +0100 wenzelm refined Markup_Tree implementation: stacked markup within each entry;
Sat, 12 Nov 2011 12:21:42 +0100 wenzelm tuned signature;
Sat, 12 Nov 2011 11:45:49 +0100 wenzelm tuned signature;
Fri, 11 Nov 2011 22:09:07 +0100 wenzelm merged
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip