23 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2017-07-17 eberlm 2017-07-17 Printing natural numbers as numerals in evaluation
2016-12-08 bulwahn 2016-12-08 filter non-matching prems to not fail in proof procedure; include test case (related to c8a93680b80d)
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2016-01-10 Lukas Bulwahn 2016-01-10 filter non-matching prems rather than fail in proof procedure in rare cases; include derived example motivating change and some similar other ones
2015-06-24 wenzelm 2015-06-24 clarified 'case' command;
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2014-05-09 haftmann 2014-05-09 hardcoded nbe and sml into value command
2014-04-24 blanchet 2014-04-24 avoid name shadowing
2014-03-06 blanchet 2014-03-06 renamed 'map_pair' to 'map_prod'
2013-02-15 haftmann 2013-02-15 less customary term_of conversions; spurious side effect on method reflection
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2012-04-03 griff 2012-04-03 renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-01 haftmann 2012-03-01 more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
2011-12-24 haftmann 2011-12-24 adjusted to set/pred distinction by means of type constructor `set`
2011-09-14 hoelzl 2011-09-14 renamed Complete_Lattices lemmas, removed legacy names
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-04-23 wenzelm 2011-04-23 modernized specifications;
2011-04-04 krauss 2011-04-04 raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.
2011-03-28 krauss 2011-03-28 raised various timeouts to accommodate sluggish SML/NJ
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-12-02 haftmann 2010-12-02 adapted expected value to more idiomatic numeral representation
2010-10-25 bulwahn 2010-10-25 changing test parameters in examples to get to a result within the global timelimit
2010-10-22 bulwahn 2010-10-22 updating to new notation in commented examples
2010-09-30 bulwahn 2010-09-30 adding example for case expressions
2010-09-29 bulwahn 2010-09-29 added test case for predicate arguments in higher-order argument position
2010-09-29 bulwahn 2010-09-29 added a test case to Predicate_Compile_Tests
2010-09-28 bulwahn 2010-09-28 adding test case for interpretation of arguments that are predicates simply as input
2010-09-28 bulwahn 2010-09-28 handling higher-order relations in output terms; improving proof procedure; added test case
2010-09-23 bulwahn 2010-09-23 moving the preprocessing of introduction rules after the code_pred command; added tuple expansion preprocessing of elimination rule
2010-09-23 bulwahn 2010-09-23 splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests