2011-07-06 bulwahn 2011-07-06 tuning options to avoid spurious isabelle test failures
2011-07-06 wenzelm 2011-07-06 clarified record syntax: fieldext excludes the "more" pseudo-field (unlike 2f885b7e5ba7), so that errors like (| x = a, more = b |) are reported less confusingly;
2011-07-06 wenzelm 2011-07-06 prefer Synchronized.var;
2011-07-06 wenzelm 2011-07-06 tuned errors; more direct Name.uu_ for dummy abstractions;
2011-07-06 wenzelm 2011-07-06 record package: proper configuration options;
2011-07-06 wenzelm 2011-07-06 just one copy of split_args; tuned error message;
2011-07-06 wenzelm 2011-07-06 merged
2011-07-05 hoelzl 2011-07-05 rename lemma Infinite_Product_Measure.sigma_sets_subseteq, it hides Sigma_Algebra.sigma_sets_subseteq
2011-07-05 nik 2011-07-05 improved translation of lambdas in THF
2011-07-05 nik 2011-07-05 added generation of lambdas in THF
2011-07-05 nik 2011-07-05 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
2011-07-05 wenzelm 2011-07-05 simplified Symbol.iterator: produce strings, which are mostly preallocated; eliminated Symbol.CharSequence complications;
2011-07-05 wenzelm 2011-07-05 tuned comment (cf. e9f26e66692d);
2011-07-05 wenzelm 2011-07-05 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
2011-07-05 wenzelm 2011-07-05 theory name needs to conform to Path syntax;
2011-07-05 wenzelm 2011-07-05 hard-wired print mode "xsymbols" increases chance that "iff" in HOL will print symbolic arrow;
2011-07-05 wenzelm 2011-07-05 prefer space_explode/split_lines as in Isabelle/ML;
2011-07-05 wenzelm 2011-07-05 Path.split convenience;
2011-07-05 wenzelm 2011-07-05 get theory from last executation state; tuned error messages;
2011-07-05 wenzelm 2011-07-05 explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example); reduced Theory.end_theory to plain projection, outside transaction context (see also ddc3b72f9a42);
2011-07-05 wenzelm 2011-07-05 clarified cancel_execution/await_cancellation;
2011-07-05 wenzelm 2011-07-05 tuned signature; tuned;
2011-07-05 wenzelm 2011-07-05 tuned;
2011-07-05 krauss 2011-07-05 re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
2011-07-04 wenzelm 2011-07-04 Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
2011-07-04 wenzelm 2011-07-04 quasi-static Isabelle_System -- reduced tendency towards "functorial style";
2011-07-04 wenzelm 2011-07-04 explicit class Counter;
2011-07-04 wenzelm 2011-07-04 merged
2011-07-04 hoelzl 2011-07-04 the borel probability measure is easier to handle with {0 ..< 1} (coverable by disjoint intervals {_ ..< _})
2011-07-04 hoelzl 2011-07-04 equalities of subsets of atLeastLessThan
2011-07-03 bulwahn 2011-07-03 adding documentation of the value antiquotation to the code generation manual
2011-07-03 blanchet 2011-07-03 make SML/NJ happy
2011-07-02 haftmann 2011-07-02 install case certificate for If after code_datatype declaration for bool
2011-07-02 haftmann 2011-07-02 tuned typo
2011-07-04 wenzelm 2011-07-04 pervasive Basic_Library in Scala; tuned;
2011-07-04 wenzelm 2011-07-04 some support for theory files within Isabelle/Scala session;
2011-07-04 wenzelm 2011-07-04 imitate exception ERROR of Isabelle/ML;
2011-07-03 wenzelm 2011-07-03 eliminated null;
2011-07-03 wenzelm 2011-07-03 more explicit edit_node vs. init_node; some support for master_dir and header;
2011-07-03 wenzelm 2011-07-03 tuned signature;
2011-07-02 wenzelm 2011-07-02 Thy_Header.read convenience;
2011-07-02 wenzelm 2011-07-02 some support for Session.File_Store;
2011-07-02 wenzelm 2011-07-02 tuned signature;
2011-07-02 wenzelm 2011-07-02 eliminated redundant session_ready;
2011-07-02 wenzelm 2011-07-02 tuned;
2011-07-02 wenzelm 2011-07-02 uniform finish_thy -- always Global_Theory.join_proofs, even with sequential scheduling;
2011-07-02 wenzelm 2011-07-02 misc tuning;
2011-07-02 haftmann 2011-07-02 correction: do not assume that case const index covered all cases
2011-07-01 haftmann 2011-07-01 remove illegal case combinators after merge
2011-07-01 haftmann 2011-07-01 corrected misunderstanding what `old functions` are supposed to be
2011-07-01 haftmann 2011-07-01 centralized deletion of equations for constructors; corrected misunderstanding what `old functions` are supposed to be
2011-07-01 haftmann 2011-07-01 merged
2011-07-01 haftmann 2011-07-01 index cases for constructors
2011-07-01 noschinl 2011-07-01 cover induct's "arbitrary" more deeply
2011-07-01 wenzelm 2011-07-01 merged;
2011-07-01 blanchet 2011-07-01 enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
2011-07-01 blanchet 2011-07-01 made minimizer informative output accurate
2011-07-01 blanchet 2011-07-01 test a few more type encodings
2011-07-01 blanchet 2011-07-01 further repair "mangled_tags", now that tags are also mangled
2011-07-01 blanchet 2011-07-01 update documentation after "type_enc" renaming + fixed a few other out-of-date factlets