2012-02-26 haftmann 2012-02-26 marked candidates for rule declarations
2012-02-26 wenzelm 2012-02-26 include warning messages in node status;
2012-02-26 wenzelm 2012-02-26 tuned signature (in accordance with ML);
2012-02-26 wenzelm 2012-02-26 more PIDE modules;
2012-02-26 wenzelm 2012-02-26 tuned proofs;
2012-02-26 wenzelm 2012-02-26 more abstract class Document.State;
2012-02-26 wenzelm 2012-02-26 more abstract class Document.State.Assignment;
2012-02-26 wenzelm 2012-02-26 tuned signature;
2012-02-26 wenzelm 2012-02-26 more abstract class Document.Version; tuned (NB: Version.nodes is total);
2012-02-26 wenzelm 2012-02-26 more abstract class Document.Node;
2012-02-26 wenzelm 2012-02-26 more abstract class Document.History;
2012-02-26 wenzelm 2012-02-26 more abstract class Document.Change;
2012-02-26 wenzelm 2012-02-26 tuned;
2012-02-26 wenzelm 2012-02-26 tuned signature; clarified check;
2012-02-25 wenzelm 2012-02-25 merged
2012-02-25 bulwahn 2012-02-25 slightly changing the enumeration scheme
2012-02-25 bulwahn 2012-02-25 adding some more test invocations of find_unused_assms
2012-02-25 bulwahn 2012-02-25 adding an example where random beats exhaustive testing
2012-02-25 bulwahn 2012-02-25 removing unnecessary assumptions in RComplete; simplifying proof in Probability
2012-02-25 bulwahn 2012-02-25 removing unnecessary assumptions in RealDef; simplifying proofs in Float, MIR, and Ferrack
2012-02-25 bulwahn 2012-02-25 one general list_all2_update_cong instead of two special ones
2012-02-25 wenzelm 2012-02-25 tuned comments;
2012-02-25 wenzelm 2012-02-25 standard Graph instances;
2012-02-25 wenzelm 2012-02-25 clarified signature -- avoid oddities of Iterable like Iterator.map; specific toString;
2012-02-25 wenzelm 2012-02-25 discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);
2012-02-24 haftmann 2012-02-24 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-24 haftmann 2012-02-24 explicit is better than implicit
2012-02-24 haftmann 2012-02-24 dropped dead code
2012-02-24 wenzelm 2012-02-24 prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty; discontinued map_nodes, del_nodes conveniences -- avoid inefficient mapValues wrapper (this is not Table.map from ML); tuned signature;
2012-02-24 wenzelm 2012-02-24 tuned imports;
2012-02-24 wenzelm 2012-02-24 tuned signature;
2012-02-24 wenzelm 2012-02-24 discontinued obsolete Graph.all_paths (last seen in 1524d69783d3 and AFP/80bbbdbfec62);
2012-02-24 wenzelm 2012-02-24 merged
2012-02-24 huffman 2012-02-24 remove ill-formed lemmas word_0_wi_Pls and word_m1_wi_Min
2012-02-24 huffman 2012-02-24 avoid using Int.succ_def in proofs
2012-02-24 huffman 2012-02-24 avoid using Int.succ or Int.pred in proofs
2012-02-24 huffman 2012-02-24 avoid using BIT_simps in proofs; rephrase lemmas without Int.succ or Int.pred;
2012-02-24 huffman 2012-02-24 avoid using BIT_simps in proofs
2012-02-24 wenzelm 2012-02-24 updated stats according to src/HOL/IsaMakefile;
2012-02-24 wenzelm 2012-02-24 more precise clean target;
2012-02-24 wenzelm 2012-02-24 clarifed name space "type name", which covers logical and non-logical types, and often occurs inside outer syntax "type" markup;
2012-02-24 huffman 2012-02-24 avoid using Int.Pls_def in proofs
2012-02-24 huffman 2012-02-24 remove ill-formed lemmas word_pred_0_Min and word_m1_Min
2012-02-24 huffman 2012-02-24 remove ill-formed lemma of_bl_no; adapt proofs
2012-02-24 huffman 2012-02-24 adapt lemma mask_lem to respect int/bin distinction
2012-02-24 blanchet 2012-02-24 rephrase some slow "metis" calls
2012-02-24 blanchet 2012-02-24 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
2012-02-24 blanchet 2012-02-24 general solution to the arity bug that occasionally plagues Sledgehammer -- short story, lots of things go kaputt when a polymorphic symbol's arity in the translation is higher than the arity of the fully polymorphic HOL constant
2012-02-24 blanchet 2012-02-24 renamed 'try_methods' to 'try0'
2012-02-24 blanchet 2012-02-24 doc fixes (thanks to Nik)
2012-02-24 blanchet 2012-02-24 fixed arity bug with "If" helpers for "If" that returns a function
2012-02-24 haftmann 2012-02-24 given up disfruitful branch
2012-02-24 haftmann 2012-02-24 explicit remove of lattice notation
2012-02-24 haftmann 2012-02-24 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-23 haftmann 2012-02-23 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-23 haftmann 2012-02-23 dropped dead code
2012-02-23 wenzelm 2012-02-23 tuned isatest settings;
2012-02-23 wenzelm 2012-02-23 merged
2012-02-23 haftmann 2012-02-23 moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
2012-02-23 haftmann 2012-02-23 tuned whitespace