2012-04-05 huffman 2012-04-05 define reflp directly, in the manner of symp and transp
2012-04-05 huffman 2012-04-05 set up and use lift_definition for word operations
2012-04-05 huffman 2012-04-05 lift_definition declares transfer_rule attribute
2012-04-05 huffman 2012-04-05 configure transfer method for 'a word -> int
2012-04-05 krauss 2012-04-05 added timestamps to logging of named thms
2012-04-05 huffman 2012-04-05 merged
2012-04-04 huffman 2012-04-04 merged
2012-04-04 huffman 2012-04-04 add lemmas for generating transfer rules for typedefs
2012-04-05 sultana 2012-04-05 tuned;
2012-04-04 sultana 2012-04-04 improved import_tptp to use standard TPTP directory structure; extended the TPTP testing theory to include an example of using the import_tptp command;
2012-04-04 Cezary Kaliszyk 2012-04-04 merge
2012-04-04 Cezary Kaliszyk 2012-04-04 HOL/Import more precise map types
2012-04-04 Cezary Kaliszyk 2012-04-04 HOL/Import typed matches against Isabelle typedef result
2012-04-04 kuncar 2012-04-04 connect the Quotient package to the Lifting package
2012-04-04 kuncar 2012-04-04 support non-open typedefs; define cr_rel in terms of a rep function for typedefs
2012-04-04 sultana 2012-04-04 tuned;
2012-04-04 sultana 2012-04-04 added interpretation for formula conditional;
2012-04-04 sultana 2012-04-04 refactored tptp lex;
2012-04-04 sultana 2012-04-04 refactored tptp yacc to bring close to official spec;
2012-04-04 huffman 2012-04-04 transfer method generalizes over free variables in goal
2012-04-04 huffman 2012-04-04 add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
2012-04-04 huffman 2012-04-04 update keywords file
2012-04-04 huffman 2012-04-04 merged
2012-04-04 huffman 2012-04-04 fix typos
2012-04-04 huffman 2012-04-04 lift_definition command generates transfer rule
2012-04-04 huffman 2012-04-04 prove_quot_theorem fixes types
2012-04-04 bulwahn 2012-04-04 documenting options quickcheck_locale; adjusting IsarRef documentation of Quotient predicate; NEWS
2012-04-04 bulwahn 2012-04-04 added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck; added examples of quickcheck_locale option; trying to speed up Quickcheck_Examples;
2012-04-06 wenzelm 2012-04-06 stop node execution at first unassigned exec;
2012-04-06 wenzelm 2012-04-06 discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;
2012-04-05 wenzelm 2012-04-05 more scalable execute/update: avoid redundant traversal of invisible/finished nodes; tuned;
2012-04-05 wenzelm 2012-04-05 less ambitious memo_eval, since memo_result is still not robust here;
2012-04-05 wenzelm 2012-04-05 less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
2012-04-05 wenzelm 2012-04-05 more explicit memo_eval vs. memo_result, to enforce bottom-up execution; edit of perspective touches node superficially, to ensure revisit after update;
2012-04-05 wenzelm 2012-04-05 Command.memo including physical interrupts (unlike Lazy.lazy); re-assign unstable exec, i.e. reset interrupted transaction; node result as direct exec -- avoid potential interrupt instability of Lazy.map;
2012-04-05 wenzelm 2012-04-05 tuned;
2012-04-04 wenzelm 2012-04-04 tuned -- NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;
2012-04-04 wenzelm 2012-04-04 proper signature constraint;
2012-04-04 wenzelm 2012-04-04 tuned comments;
2012-04-04 wenzelm 2012-04-04 separate module for prover command execution;
2012-04-04 wenzelm 2012-04-04 tuned;
2012-04-04 huffman 2012-04-04 fix typo in ML structure name
2012-04-04 wenzelm 2012-04-04 removed obsolete isar-overview manual;
2012-04-04 sultana 2012-04-04 dealing with SMLNJ errors 'value type in structure doesn't match signature spec' (which originated from lack of type generalisation) and 'unresolved flex record' wrt tptp_interpret
2012-04-04 bulwahn 2012-04-04 merged
2012-04-04 bulwahn 2012-04-04 rudimentary handling of products in finitize_functions in Quickcheck-Narrowing
2012-04-04 bulwahn 2012-04-04 improved equality check for modes in predicate compiler
2012-04-04 huffman 2012-04-04 rename ML structure to avoid shadowing earlier name
2012-04-04 huffman 2012-04-04 add type annotations to make SML happy (cf. ec6187036495)
2012-04-03 huffman 2012-04-03 merged
2012-04-03 huffman 2012-04-03 new transfer proof method
2012-04-03 huffman 2012-04-03 renamed Tools/transfer.ML to Tools/legacy_transfer.ML
2012-04-03 wenzelm 2012-04-03 prefer prog-prove, suppress isar-overview;
2012-04-03 wenzelm 2012-04-03 merged
2012-04-03 wenzelm 2012-04-03 merged
2012-04-03 wenzelm 2012-04-03 formal integration of "prog-prove" manual; "main" is a reference manual;
2012-04-03 wenzelm 2012-04-03 prefer static dependencies;
2012-04-03 huffman 2012-04-03 merged
2012-04-03 huffman 2012-04-03 modernized obsolete old-style theory name with proper new-style underscore
2012-04-03 sultana 2012-04-03 removed use of CharVector in generated parser, to make SMLNJ happy