2010-04-28 ago wenzelm localized default sort;
2010-04-28 ago wenzelm more systematic naming of tsig operations;
2010-04-28 ago wenzelm modernized/simplified Sign.set_defsort;
2010-04-28 ago wenzelm get_sort: minimize sorts given in the text, while keeping those from the context unchanged (the latter are preferred);
2010-04-28 ago wenzelm export Type.minimize_sort;
2010-04-28 ago haftmann term_typ: print styled term
2010-04-27 ago wenzelm merged
2010-04-27 ago huffman merged
2010-04-27 ago huffman generalize types of path operations
2010-04-27 ago huffman generalize more continuity lemmas
2010-04-27 ago huffman generalized many lemmas about continuity
2010-04-26 ago huffman simplify definition of continuous_on; generalize some lemmas
2010-04-26 ago huffman move intervals section heading
2010-04-26 ago huffman remove unused, redundant constant inv_on
2010-04-26 ago huffman reorganize subsection headings
2010-04-26 ago huffman remove redundant lemma
2010-04-26 ago huffman more lemmas to Vec1.thy
2010-04-26 ago huffman simplify proof
2010-04-26 ago huffman move more lemmas into Vec1.thy
2010-04-26 ago huffman move proof of Fashoda meet theorem into separate file
2010-04-26 ago huffman move definitions and theorems for type real^1 to separate theory file
2010-04-27 ago wenzelm removed obsolete sanity check -- Sign.certify_sort is stable;
2010-04-27 ago wenzelm monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
2010-04-27 ago wenzelm really minimize sorts after certification -- looks like this is intended here;
2010-04-27 ago wenzelm tuned signature;
2010-04-27 ago wenzelm merged
2010-04-27 ago haftmann tuned whitespace
2010-04-27 ago haftmann got rid of [simplified]
2010-04-27 ago haftmann got rid of [simplified]
2010-04-27 ago blanchet fix SML/NJ compilation (I hope)
2010-04-27 ago wenzelm tuned classrel completion -- bypass composition with reflexive edges;
2010-04-27 ago wenzelm tuned diff_classrels -- avoid slightly inefficient Symreltab.keys;
2010-04-27 ago wenzelm tuned aritiy completion -- slightly less intermediate data structures;
2010-04-27 ago wenzelm clarified proven results: store thm only and retrieve proof later via Thm.proof_of (this may also impact parallelism, because internal join_proofs is deferred);
2010-04-27 ago wenzelm misc tuning and simplification;
2010-04-27 ago haftmann NEWS and CONTRIBUTORS
2010-04-27 ago haftmann explicit is better than implicit
2010-04-27 ago haftmann tuned class linordered_field_inverse_zero
2010-04-27 ago haftmann merged
2010-04-27 ago haftmann instances for *_inverse_zero classes
2010-04-27 ago haftmann canonical import
2010-04-26 ago haftmann merged
2010-04-26 ago haftmann use new classes (linordered_)field_inverse_zero
2010-04-26 ago blanchet merged
2010-04-26 ago blanchet renamed option
2010-04-26 ago blanchet fixes 2a5c6e7b55cb;
2010-04-26 ago blanchet compile
2010-04-26 ago blanchet make compile (and not just load dynamically)
2010-04-26 ago blanchet merge
2010-04-26 ago blanchet introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
2010-04-26 ago blanchet adapt code to reflect new signature of "neg_clausify"
2010-04-26 ago blanchet rename options and keep track of conjecture shape (to facilitate proof reconstruction)
2010-04-26 ago blanchet rename options
2010-04-26 ago blanchet make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
2010-04-26 ago blanchet remove needless code that was copy-pasted from Quickcheck (where it made sense)
2010-04-25 ago blanchet cosmetics
2010-04-25 ago blanchet cosmetics
2010-04-25 ago blanchet move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
2010-04-25 ago blanchet support readable names even when Isar proof reconstruction is enabled -- useful for debugging
2010-04-25 ago blanchet cosmetics: rename internal functions