2012-04-03 griff 2012-04-03 dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
2012-04-03 griff 2012-04-03 renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
2012-04-12 wenzelm 2012-04-12 more standard method setup;
2012-04-12 wenzelm 2012-04-12 more precise declaration of goal_tfrees in forked proof state;
2012-04-12 wenzelm 2012-04-12 partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
2012-04-12 bulwahn 2012-04-12 multiset operations are defined with lift_definitions; tuned proofs;
2012-04-12 huffman 2012-04-12 remove outdated comment
2012-04-11 wenzelm 2012-04-11 rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
2012-04-11 wenzelm 2012-04-11 standardized ML aliases;
2012-04-11 wenzelm 2012-04-11 clarified proof_result: finish proof formally via head tr, not end_tr;
2012-04-11 wenzelm 2012-04-11 tuned;
2012-04-11 wenzelm 2012-04-11 more robust Future.fulfill wrt. duplicate assignment and interrupt;
2012-04-11 wenzelm 2012-04-11 tuned message;
2012-04-11 wenzelm 2012-04-11 always signal after cancel_group: passive tasks may have become active;
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