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
Fri, 11 Nov 2011 12:31:00 +0100 huffman merged
Fri, 11 Nov 2011 12:30:28 +0100 huffman abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
Fri, 11 Nov 2011 11:30:31 +0100 huffman use simproc_setup for the remaining nat_numeral simprocs
Fri, 11 Nov 2011 11:11:03 +0100 huffman use simproc_setup for more nat_numeral simprocs; add simproc tests
Fri, 11 Nov 2011 12:10:49 +0100 bulwahn using more conventional names for monad plus operations
Fri, 11 Nov 2011 22:05:18 +0100 wenzelm more tooltip content;
Fri, 11 Nov 2011 21:45:52 +0100 wenzelm added markup_cumulate operator;
Fri, 11 Nov 2011 16:25:32 +0100 wenzelm depth-first proof forking for improved locality (wrt. cancellation and overall memory usage);
Fri, 11 Nov 2011 16:06:26 +0100 wenzelm tuned;
Fri, 11 Nov 2011 15:25:22 +0100 wenzelm more abstract Markup_Tree;
Fri, 11 Nov 2011 14:24:38 +0100 wenzelm prefer statically typed Text.Markup;
Fri, 11 Nov 2011 14:07:20 +0100 wenzelm discontinued entity text color, notably historic red for classes;
Fri, 11 Nov 2011 12:52:57 +0100 wenzelm more scalable Proof_Context.prepare_sorts;
Fri, 11 Nov 2011 10:40:36 +0100 bulwahn increasing values_timeout to avoid failures of isatest with HOL-IMP
Fri, 11 Nov 2011 08:32:48 +0100 bulwahn renaming example invocations: tester predicate_compile is renamed to smart_exhaustive
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip