src/HOL/Tools/Predicate_Compile/code_prolog.ML
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-12-19 wenzelm 2014-12-19 more standard configuration options;
2014-11-03 wenzelm 2014-11-03 eliminated unused int_only flag (see also c12484a27367); just proper commands;
2014-08-16 wenzelm 2014-08-16 updated to named_theorems;
2014-05-01 haftmann 2014-05-01 centralized upper/lowercase name mangling
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-02-17 wenzelm 2014-02-17 made SML/NJ happy;
2014-02-13 wenzelm 2014-02-13 removed dead code;
2014-02-13 wenzelm 2014-02-13 do not redefine outer syntax commands;
2014-02-13 wenzelm 2014-02-13 static repair of ML file -- untested (!) by default since 76965c356d2a;
2014-02-12 wenzelm 2014-02-12 merged, resolving some conflicts;
2014-02-12 wenzelm 2014-02-12 tuned whitespace;
2014-02-12 blanchet 2014-02-12 ported predicate compiler to 'ctr_sugar' * * * ported predicate compiler to 'ctr_sugar', part 2
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
2013-04-16 wenzelm 2013-04-16 proper prolog command-line instead of hashbang, which might switch to invalid executable and thus fail (notably on lxbroy2); speculative update for yap (untested);
2013-04-12 wenzelm 2013-04-12 actually fail on prolog errors -- such as swipl startup failure due to missing shared libraries -- assuming it normally produces clean return code 0;
2013-02-28 wenzelm 2013-02-28 just one HOLogic.Trueprop_conv, with regular exception CTERM; tuned;
2013-02-14 haftmann 2013-02-14 reform of predicate compiler / quickcheck theories: implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers! avoid odd New_ prefix by joining related theories; avoid overcompact name DSequence; separated predicate inside random monad into separate theory; consolidated name of theory Quickcheck
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-15 wenzelm 2012-03-15 prefer formally checked @{keyword} parser;
2012-02-23 wenzelm 2012-02-23 clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
2011-12-04 bulwahn 2011-12-04 adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e); adjusting smart quickcheck compilation to new signature of exhaustive generators (cf. 1f5fc44254d7);
2011-11-10 bulwahn 2011-11-10 renewed prolog-quickcheck
2011-10-21 bulwahn 2011-10-21 correcting code_prolog
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2011-07-18 bulwahn 2011-07-18 adapting prolog-based tester
2011-07-16 wenzelm 2011-07-16 moved bash operations to Isabelle_System (cf. Scala version);
2011-07-09 bulwahn 2011-07-09 standardized String.concat towards implode (cf. c37a1f29bbc0)
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2011-04-27 wenzelm 2011-04-27 some adhoc renaming, to accomodate more strict checks of fixes (cf. 4638622bcaa1);
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-30 bulwahn 2011-03-30 generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
2011-03-26 wenzelm 2011-03-26 Isabelle_System.create_tmp_path/with_tmp_file: optional extension; thread-safe versions of Present.display_graph, Present.isabelle_browser, Present.drafts -- using Isabelle_System.with_tmp_dir;
2011-03-25 bulwahn 2011-03-25 revisiting Code_Prolog (cf. 6fe4abb9437b)
2011-03-23 bulwahn 2011-03-23 adapting Quickcheck_Prolog to latest changes
2011-03-13 wenzelm 2011-03-13 cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection; determine swipl_version at runtime;
2011-03-13 wenzelm 2011-03-13 tuned headers;
2011-03-13 wenzelm 2011-03-13 allow spaces in executable names; simplified generated bash scripts;
2011-01-08 wenzelm 2011-01-08 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2010-12-20 wenzelm 2010-12-20 slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version); more robust rm_tree -- somewhat dangerous and not exported; tuned;
2010-12-07 wenzelm 2010-12-07 eliminated some hard tabulators (deprecated);
2010-12-03 bulwahn 2010-12-03 adapting predicate_compile_quickcheck
2010-11-02 wenzelm 2010-11-02 simplified some time constants;
2010-10-21 bulwahn 2010-10-21 adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
2010-09-30 bulwahn 2010-09-30 adding option to globally limit the prolog execution
2010-09-28 bulwahn 2010-09-28 renaming use_random to use_generators in the predicate compiler
2010-09-27 bulwahn 2010-09-27 adding further tracing messages; tuned
2010-09-20 bulwahn 2010-09-20 renaming variable name to decrease likelyhood of nameclash
2010-09-20 bulwahn 2010-09-20 moving renaming_vars to post_processing; removing clone in values and quickcheck of code_prolog
2010-09-20 bulwahn 2010-09-20 removing clone in code_prolog and predicate_compile_quickcheck
2010-09-16 bulwahn 2010-09-16 adding restoring of numerals for natural numbers for values command
2010-09-16 bulwahn 2010-09-16 values command for prolog supports complex terms and not just variables
2010-09-16 bulwahn 2010-09-16 registering code_prolog as component; using environment variable; adding settings file for prolog code generation
2010-09-16 bulwahn 2010-09-16 adding mode inference to prolog compilation; separate between (ad-hoc) code modifications and system_configuration; adapting quickcheck
2010-09-15 bulwahn 2010-09-15 adding option show_invalid_clauses for a more detailed message when modes are not inferred
2010-09-07 bulwahn 2010-09-07 towards time limiting the prolog execution
2010-09-07 bulwahn 2010-09-07 adding dependencies to IsaMakefile; increasing negative search limit for predicate_compile_quickcheck; adding tracing of introduction rules in code_prolog