2010-04-28 haftmann 2010-04-28 exported cert_tyco, read_tyco
2010-04-28 haftmann 2010-04-28 added code_reflect command
2010-04-28 haftmann 2010-04-28 merged
2010-04-28 haftmann 2010-04-28 fix "fors" for proof of monotonicity
2010-04-28 Cezary Kaliszyk 2010-04-28 merge
2010-04-28 Cezary Kaliszyk 2010-04-28 merge
2010-04-28 Cezary Kaliszyk 2010-04-28 Tuned FSet
2010-04-28 haftmann 2010-04-28 merged
2010-04-28 haftmann 2010-04-28 try to observe intended meaning of add_registration interface more closely
2010-04-28 haftmann 2010-04-28 codified comment
2010-04-28 haftmann 2010-04-28 merged
2010-04-28 haftmann 2010-04-28 empty class specifcations observe default sort
2010-04-28 wenzelm 2010-04-28 document some known problems with Mac OS;
2010-04-28 wenzelm 2010-04-28 removed redundant/ignored sort constraint;
2010-04-28 wenzelm 2010-04-28 tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
2010-04-28 wenzelm 2010-04-28 made SML/NJ happy;
2010-04-28 wenzelm 2010-04-28 updated keywords;
2010-04-28 wenzelm 2010-04-28 command 'defaultsort' is renamed to 'default_sort', it works within a local theory context;
2010-04-28 wenzelm 2010-04-28 removed material that is out of scope of this manual;
2010-04-28 wenzelm 2010-04-28 renamed command 'defaultsort' to 'default_sort';
2010-04-28 wenzelm 2010-04-28 localized default sort;
2010-04-28 wenzelm 2010-04-28 more systematic naming of tsig operations;
2010-04-28 wenzelm 2010-04-28 modernized/simplified Sign.set_defsort;
2010-04-28 wenzelm 2010-04-28 get_sort: minimize sorts given in the text, while keeping those from the context unchanged (the latter are preferred); tuned;
2010-04-28 wenzelm 2010-04-28 export Type.minimize_sort;
2010-04-28 haftmann 2010-04-28 term_typ: print styled term
2010-04-27 wenzelm 2010-04-27 merged
2010-04-27 huffman 2010-04-27 merged
2010-04-27 huffman 2010-04-27 generalize types of path operations
2010-04-27 huffman 2010-04-27 generalize more continuity lemmas
2010-04-27 huffman 2010-04-27 generalized many lemmas about continuity
2010-04-26 huffman 2010-04-26 simplify definition of continuous_on; generalize some lemmas
2010-04-26 huffman 2010-04-26 move intervals section heading
2010-04-26 huffman 2010-04-26 remove unused, redundant constant inv_on
2010-04-26 huffman 2010-04-26 reorganize subsection headings
2010-04-26 huffman 2010-04-26 remove redundant lemma
2010-04-26 huffman 2010-04-26 more lemmas to Vec1.thy
2010-04-26 huffman 2010-04-26 simplify proof
2010-04-26 huffman 2010-04-26 move more lemmas into Vec1.thy
2010-04-26 huffman 2010-04-26 move proof of Fashoda meet theorem into separate file
2010-04-26 huffman 2010-04-26 move definitions and theorems for type real^1 to separate theory file
2010-04-27 wenzelm 2010-04-27 removed obsolete sanity check -- Sign.certify_sort is stable;
2010-04-27 wenzelm 2010-04-27 monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
2010-04-27 wenzelm 2010-04-27 really minimize sorts after certification -- looks like this is intended here;
2010-04-27 wenzelm 2010-04-27 tuned signature;
2010-04-27 wenzelm 2010-04-27 merged
2010-04-27 haftmann 2010-04-27 tuned whitespace
2010-04-27 haftmann 2010-04-27 got rid of [simplified]
2010-04-27 haftmann 2010-04-27 got rid of [simplified]
2010-04-27 blanchet 2010-04-27 fix SML/NJ compilation (I hope)
2010-04-27 wenzelm 2010-04-27 tuned classrel completion -- bypass composition with reflexive edges;
2010-04-27 wenzelm 2010-04-27 tuned diff_classrels -- avoid slightly inefficient Symreltab.keys;
2010-04-27 wenzelm 2010-04-27 tuned aritiy completion -- slightly less intermediate data structures;
2010-04-27 wenzelm 2010-04-27 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 wenzelm 2010-04-27 misc tuning and simplification;
2010-04-27 haftmann 2010-04-27 NEWS and CONTRIBUTORS
2010-04-27 haftmann 2010-04-27 explicit is better than implicit
2010-04-27 haftmann 2010-04-27 tuned class linordered_field_inverse_zero
2010-04-27 haftmann 2010-04-27 merged
2010-04-27 haftmann 2010-04-27 instances for *_inverse_zero classes