2012-04-11 wenzelm 2012-04-11 just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update; explicit terminate_execution; tuned source structure;
2012-04-10 wenzelm 2012-04-10 merged
2012-04-10 Christian Urban 2012-04-10 moved lift_raw_const wrapper out of the Quotient-package into Nominal2
2012-04-10 wenzelm 2012-04-10 misc tuning and simplification;
2012-04-10 wenzelm 2012-04-10 static relevance of proof via syntax keywords;
2012-04-10 wenzelm 2012-04-10 tuned future priorities: print 0, goal ~1, execute ~2;
2012-04-10 wenzelm 2012-04-10 updated for Poly/ML SVN 1476;
2012-04-10 wenzelm 2012-04-10 some coverage of HOL/TPTP;
2012-04-10 sultana 2012-04-10 added graph-conversion utility for TPTP files
2012-04-10 sultana 2012-04-10 moved non-interpret-specific code to different module
2012-04-09 wenzelm 2012-04-09 disable parallel proofs (again) -- still suffering from instabilites wrt. interrupts;
2012-04-09 wenzelm 2012-04-09 tuned proofs;
2012-04-09 wenzelm 2012-04-09 slightly faster default compilation of Isabelle/Scala;
2012-04-09 wenzelm 2012-04-09 more explicit last exec result;
2012-04-09 wenzelm 2012-04-09 dynamic propagation of node "updated" status, which is required to propagate edits and re-assigments and allow direct memo_result; discontinued odd "touched" field -- check given edits directly;
2012-04-09 wenzelm 2012-04-09 tuned;
2012-04-09 wenzelm 2012-04-09 simplified Future.cancel/cancel_group (again) -- running threads only; more robust update/cancel_execution: full join_tasks of group before exec state assignment; tuned signature;
2012-04-09 wenzelm 2012-04-09 added ML pretty-printing;
2012-04-07 wenzelm 2012-04-07 merged
2012-04-07 wenzelm 2012-04-07 merged
2012-04-07 haftmann 2012-04-07 explicit constructor Nat leaves nat_of as conversion
2012-04-06 haftmann 2012-04-06 abandoned almost redundant *_foldr lemmas
2012-04-06 haftmann 2012-04-06 tuned
2012-04-06 haftmann 2012-04-06 no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
2012-04-07 wenzelm 2012-04-07 enable parallel proofs (cf. e8552cba702d), only affects packages so far; disable quick_and_dirty to make packages produce proofs -- NB: 'sorry' works via "int" mode of proof commands;
2012-04-07 wenzelm 2012-04-07 added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
2012-04-07 wenzelm 2012-04-07 tuned proofs;
2012-04-07 wenzelm 2012-04-07 more robust update_perspective, e.g. required after reload of buffer that is not at start position;
2012-04-07 wenzelm 2012-04-07 tuned imports;
2012-04-07 wenzelm 2012-04-07 updated header keywords;
2012-04-07 wenzelm 2012-04-07 init message not bad;
2012-04-07 wenzelm 2012-04-07 explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
2012-04-06 wenzelm 2012-04-06 discontinued obsolete last_execs (cf. cd3ab7625519);
2012-04-06 huffman 2012-04-06 remove now-unnecessary type annotations from lift_definition commands
2012-04-06 huffman 2012-04-06 more robust generation of quotient rules using tactics
2012-04-06 huffman 2012-04-06 merged
2012-04-06 huffman 2012-04-06 add function dest_Quotient
2012-04-06 wenzelm 2012-04-06 standardized alias;
2012-04-06 wenzelm 2012-04-06 fixed document;
2012-04-06 wenzelm 2012-04-06 merged
2012-04-06 huffman 2012-04-06 correct plumbing of proof contexts, so that force_rty_type won't generalize more type variables than it should
2012-04-05 kuncar 2012-04-05 detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
2012-04-05 kuncar 2012-04-05 make Quotient_Def.lift_raw_const working again
2012-04-05 huffman 2012-04-05 use standard quotient lemmas to generate transfer rules
2012-04-05 huffman 2012-04-05 add transfer lemmas for quotients
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