2011-11-15 blanchet 2011-11-15 continued implementation of lambda-lifting in Metis
2011-11-15 blanchet 2011-11-15 disable debugging output
2011-11-15 blanchet 2011-11-15 use consts, not frees, for lambda-lifting
2011-11-15 blanchet 2011-11-15 started implementing lambda-lifting in Metis
2011-11-15 bulwahn 2011-11-15 improved generators for rational numbers to generate negative numbers; added examples
2011-11-15 bulwahn 2011-11-15 tuned
2011-11-15 huffman 2011-11-15 remove one more old-style semicolon
2011-11-15 huffman 2011-11-15 Metis_Examples/Big_O.thy: add number_ring class constraints, adapt proofs to use cancellation simprocs
2011-11-15 huffman 2011-11-15 remove old-style semicolons
2011-11-15 huffman 2011-11-15 avoid theorem references like 'semiring_norm(111)'
2011-11-15 huffman 2011-11-15 merged
2011-11-14 huffman 2011-11-14 merged
2011-11-14 huffman 2011-11-14 Parametric_Ferrante_Rackoff.thy: restrict to class number_ring, replace '1+1' with '2' everywhere
2011-11-14 huffman 2011-11-14 avoid numeral-representation-specific rules in metis proof
2011-11-14 wenzelm 2011-11-14 merged
2011-11-14 hoelzl 2011-11-14 remove sorry, otherwise it breaks the testboard
2011-11-14 hoelzl 2011-11-14 cleaned up float theories; removed duplicate definitions and theorems
2011-11-14 hoelzl 2011-11-14 enforce quick_and_dirty in Code_Real_Approx_By_Float
2011-11-14 wenzelm 2011-11-14 some support for partial evaluation of attributed facts;
2011-11-14 wenzelm 2011-11-14 tuned;
2011-11-14 wenzelm 2011-11-14 eliminated dead code;
2011-11-14 wenzelm 2011-11-14 inner syntax positions for string literals;
2011-11-14 wenzelm 2011-11-14 less confusion subexpression markup;
2011-11-14 wenzelm 2011-11-14 pass positions for named targets, for formal links in the document model;
2011-11-14 wenzelm 2011-11-14 simplified Runtime.exn_messages: always print detailed version of low-level exeptions, which should not occur in regular user errors anyway;
2011-11-14 wenzelm 2011-11-14 more detailed exception_trace: in Poly/ML 5.4.x intermediate handlers reset the trace (cf. Poly/ML SVN 1110);
2011-11-14 bulwahn 2011-11-14 merged
2011-11-14 bulwahn 2011-11-14 setting up exhaustive generators which are used for the smart generators
2011-11-14 hoelzl 2011-11-14 add Code_Real_Approx_By_Float
2011-11-14 huffman 2011-11-14 merged
2011-11-13 huffman 2011-11-13 remove lemma float_remove_real_numeral, which duplicated Float.float_number_of
2011-11-13 huffman 2011-11-13 remove unnecessary number-representation-specific rules from metis calls; speed up another proof
2011-11-13 blanchet 2011-11-13 avoid confusing selector output
2011-11-13 blanchet 2011-11-13 remove unsound line in Nitpick's "rat" setup
2011-11-12 wenzelm 2011-11-12 tuned proofs;
2011-11-12 wenzelm 2011-11-12 merged
2011-11-12 huffman 2011-11-12 removed some old-style semicolons
2011-11-12 wenzelm 2011-11-12 index markup elements for more efficient cumulate/select operations;
2011-11-12 wenzelm 2011-11-12 tuned;
2011-11-12 wenzelm 2011-11-12 tuned markup -- prefer user-perspective;
2011-11-12 wenzelm 2011-11-12 tuned specifications and proofs;
2011-11-12 wenzelm 2011-11-12 more precise type;
2011-11-12 wenzelm 2011-11-12 refined Markup_Tree implementation: stacked markup within each entry; tuned;
2011-11-12 wenzelm 2011-11-12 tuned signature; express select in terms of cumulate;
2011-11-12 wenzelm 2011-11-12 tuned signature;
2011-11-11 wenzelm 2011-11-11 merged
2011-11-11 huffman 2011-11-11 merged
2011-11-11 huffman 2011-11-11 abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite; add tests for abel_cancel simprocs
2011-11-11 huffman 2011-11-11 use simproc_setup for the remaining nat_numeral simprocs
2011-11-11 huffman 2011-11-11 use simproc_setup for more nat_numeral simprocs; add simproc tests
2011-11-11 bulwahn 2011-11-11 using more conventional names for monad plus operations
2011-11-11 wenzelm 2011-11-11 more tooltip content;
2011-11-11 wenzelm 2011-11-11 added markup_cumulate operator;
2011-11-11 wenzelm 2011-11-11 depth-first proof forking for improved locality (wrt. cancellation and overall memory usage);
2011-11-11 wenzelm 2011-11-11 tuned;
2011-11-11 wenzelm 2011-11-11 more abstract Markup_Tree;
2011-11-11 wenzelm 2011-11-11 prefer statically typed Text.Markup;
2011-11-11 wenzelm 2011-11-11 discontinued entity text color, notably historic red for classes; tuned entity names;
2011-11-11 wenzelm 2011-11-11 more scalable Proof_Context.prepare_sorts; reverted a97251eea458 -- uniform position constraints independently of accidental source positions (e.g. TTY vs. document);
2011-11-11 bulwahn 2011-11-11 increasing values_timeout to avoid failures of isatest with HOL-IMP