huffman [Thu, 17 Nov 2011 05:27:45 +0100] rev 45531
merged
huffman [Wed, 16 Nov 2011 15:20:27 +0100] rev 45530
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman [Wed, 16 Nov 2011 13:58:31 +0100] rev 45529
remove redundant lemmas bin_last_mod and bin_rest_div, use bin_last_def and bin_rest_def instead
huffman [Wed, 16 Nov 2011 12:29:50 +0100] rev 45528
simplify proof of word_of_int; remove several now-unused lemmas about Rep_Integ
wenzelm [Wed, 16 Nov 2011 23:09:46 +0100] rev 45527
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
wenzelm [Wed, 16 Nov 2011 21:16:36 +0100] rev 45526
clarified Attrib.partial_evaluation;
wenzelm [Wed, 16 Nov 2011 20:56:21 +0100] rev 45525
tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
blanchet [Wed, 16 Nov 2011 17:59:58 +0100] rev 45524
compile
blanchet [Wed, 16 Nov 2011 17:26:42 +0100] rev 45523
compile
blanchet [Wed, 16 Nov 2011 17:19:08 +0100] rev 45522
compile
blanchet [Wed, 16 Nov 2011 17:06:14 +0100] rev 45521
give each time slice its own lambda translation
blanchet [Wed, 16 Nov 2011 16:35:19 +0100] rev 45520
thread in additional options to minimizer
blanchet [Wed, 16 Nov 2011 13:22:36 +0100] rev 45519
make metis reconstruction handling more flexible
blanchet [Wed, 16 Nov 2011 11:16:23 +0100] rev 45518
document metis options better
blanchet [Wed, 16 Nov 2011 10:44:36 +0100] rev 45517
fixed typo
blanchet [Wed, 16 Nov 2011 10:34:08 +0100] rev 45516
document "lam_trans" option
blanchet [Wed, 16 Nov 2011 10:09:44 +0100] rev 45515
nicer bullets
blanchet [Wed, 16 Nov 2011 09:42:27 +0100] rev 45514
parse lambda translation option in Metis
blanchet [Tue, 15 Nov 2011 22:20:58 +0100] rev 45513
rename the lambda translation schemes, so that they are understandable out of context
blanchet [Tue, 15 Nov 2011 22:15:51 +0100] rev 45512
rename configuration option to more reasonable length
blanchet [Tue, 15 Nov 2011 22:13:39 +0100] rev 45511
continued implementation of lambda-lifting in Metis
blanchet [Tue, 15 Nov 2011 22:13:39 +0100] rev 45510
disable debugging output
blanchet [Tue, 15 Nov 2011 22:13:39 +0100] rev 45509
use consts, not frees, for lambda-lifting
blanchet [Tue, 15 Nov 2011 22:13:39 +0100] rev 45508
started implementing lambda-lifting in Metis
bulwahn [Tue, 15 Nov 2011 15:38:50 +0100] rev 45507
improved generators for rational numbers to generate negative numbers;
added examples
bulwahn [Tue, 15 Nov 2011 15:38:49 +0100] rev 45506
tuned
huffman [Tue, 15 Nov 2011 12:51:14 +0100] rev 45505
remove one more old-style semicolon
huffman [Tue, 15 Nov 2011 12:49:05 +0100] rev 45504
Metis_Examples/Big_O.thy: add number_ring class constraints, adapt proofs to use cancellation simprocs
huffman [Tue, 15 Nov 2011 12:39:49 +0100] rev 45503
remove old-style semicolons
huffman [Tue, 15 Nov 2011 12:39:29 +0100] rev 45502
avoid theorem references like 'semiring_norm(111)'
huffman [Tue, 15 Nov 2011 09:22:19 +0100] rev 45501
merged
huffman [Mon, 14 Nov 2011 19:35:41 +0100] rev 45500
merged
huffman [Mon, 14 Nov 2011 19:35:05 +0100] rev 45499
Parametric_Ferrante_Rackoff.thy: restrict to class number_ring, replace '1+1' with '2' everywhere
huffman [Mon, 14 Nov 2011 09:49:05 +0100] rev 45498
avoid numeral-representation-specific rules in metis proof
wenzelm [Mon, 14 Nov 2011 23:13:23 +0100] rev 45497
merged
hoelzl [Mon, 14 Nov 2011 21:11:31 +0100] rev 45496
remove sorry, otherwise it breaks the testboard
hoelzl [Mon, 14 Nov 2011 18:36:31 +0100] rev 45495
cleaned up float theories; removed duplicate definitions and theorems
hoelzl [Mon, 14 Nov 2011 12:28:34 +0100] rev 45494
enforce quick_and_dirty in Code_Real_Approx_By_Float
wenzelm [Mon, 14 Nov 2011 23:00:56 +0100] rev 45493
some support for partial evaluation of attributed facts;
wenzelm [Mon, 14 Nov 2011 20:25:22 +0100] rev 45492
tuned;
wenzelm [Mon, 14 Nov 2011 19:27:42 +0100] rev 45491
eliminated dead code;
wenzelm [Mon, 14 Nov 2011 17:48:26 +0100] rev 45490
inner syntax positions for string literals;
wenzelm [Mon, 14 Nov 2011 17:47:59 +0100] rev 45489
less confusion subexpression markup;
wenzelm [Mon, 14 Nov 2011 16:52:19 +0100] rev 45488
pass positions for named targets, for formal links in the document model;
wenzelm [Mon, 14 Nov 2011 16:24:50 +0100] rev 45487
simplified Runtime.exn_messages: always print detailed version of low-level exeptions, which should not occur in regular user errors anyway;
wenzelm [Mon, 14 Nov 2011 16:16:49 +0100] rev 45486
more detailed exception_trace: in Poly/ML 5.4.x intermediate handlers reset the trace (cf. Poly/ML SVN 1110);
bulwahn [Mon, 14 Nov 2011 12:29:19 +0100] rev 45485
merged
bulwahn [Mon, 14 Nov 2011 11:14:06 +0100] rev 45484
setting up exhaustive generators which are used for the smart generators