2010-11-27 huffman 2010-11-27 rename function 'match_UU' to 'match_bottom'
2010-11-27 huffman 2010-11-27 rename function 'strict' to 'seq', which is its name in Haskell
2010-11-27 haftmann 2010-11-27 merged
2010-11-27 haftmann 2010-11-27 merged
2010-11-27 haftmann 2010-11-27 typscheme with signatures is inappropriate when building empty certificate; prefer logical_typscheme over const_typargs; tuned
2010-11-27 haftmann 2010-11-27 merged
2010-11-27 haftmann 2010-11-27 merged
2010-11-27 haftmann 2010-11-27 corrected: use canonical variables of type scheme uniformly
2010-11-27 haftmann 2010-11-27 tuned
2010-11-26 haftmann 2010-11-26 merged
2010-11-26 haftmann 2010-11-26 consider sort constraints for datatype constructors when constructing the empty equation certificate; actually consider sort constraints in constructor sets; dropped redundant bindings
2010-11-26 haftmann 2010-11-26 tuned example
2010-11-27 wenzelm 2010-11-27 merged
2010-11-27 haftmann 2010-11-27 updated generated documents
2010-11-27 haftmann 2010-11-27 added equation for Queue; tuned proofs
2010-11-27 haftmann 2010-11-27 added evaluation section
2010-11-27 haftmann 2010-11-27 tuned formatting; adjustments to changes on ML level
2010-11-27 haftmann 2010-11-27 added label
2010-11-27 wenzelm 2010-11-27 more thorough process termination (cf. Scala version);
2010-11-27 wenzelm 2010-11-27 prefer Isabelle/ML concurrency elements; more careful propagation of interrupts;
2010-11-27 wenzelm 2010-11-27 removed bash from ML system bootstrap, and past the Secure ML barrier;
2010-11-27 wenzelm 2010-11-27 more proper int wrappers;
2010-11-27 wenzelm 2010-11-27 explicit check for requirement;
2010-11-27 wenzelm 2010-11-27 more basic Isabelle_System.mkdir;
2010-11-27 wenzelm 2010-11-27 tuned;
2010-11-27 wenzelm 2010-11-27 more explicit Isabelle_System operations;
2010-11-27 wenzelm 2010-11-27 prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
2010-11-27 wenzelm 2010-11-27 moved file identification to thy_load.ML (where it is actually used);
2010-11-27 wenzelm 2010-11-27 removed some old settings;
2010-11-27 wenzelm 2010-11-27 recovered global "Isabelle" symlink for isatest (cf. 7f745e4b7cce);
2010-11-26 huffman 2010-11-26 merged
2010-11-26 huffman 2010-11-26 remove map function names from domain package theory data
2010-11-26 huffman 2010-11-26 isar-style proof for lemma contI2
2010-11-26 huffman 2010-11-26 remove case combinator for fixrec match type
2010-11-26 huffman 2010-11-26 declare more simp rules for powerdomains
2010-11-27 wenzelm 2010-11-27 merged; adapted ListPair.UnequalLengths;
2010-11-26 haftmann 2010-11-26 merged
2010-11-26 haftmann 2010-11-26 strict forall2
2010-11-26 haftmann 2010-11-26 nbe decides equality of abstractions by extensionality
2010-11-26 wenzelm 2010-11-26 eliminated some generated comments;
2010-11-26 wenzelm 2010-11-26 merged
2010-11-26 haftmann 2010-11-26 merged
2010-11-26 haftmann 2010-11-26 keep type variable arguments of datatype constructors in bookkeeping
2010-11-26 blanchet 2010-11-26 document changes in Nitpick and MESON/Metis
2010-11-26 blanchet 2010-11-26 renamed "trace_me{son,tis}" and "verbose_metis" to have the name of the tool first
2010-11-26 blanchet 2010-11-26 put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
2010-11-26 wenzelm 2010-11-26 make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-11-26 wenzelm 2010-11-26 just one version of fold_rev2;
2010-11-26 wenzelm 2010-11-26 explicit use of unprefix;
2010-11-26 wenzelm 2010-11-26 keep private things private, without comments;
2010-11-26 wenzelm 2010-11-26 eliminated some clones of eq_list;
2010-11-26 nipkow 2010-11-26 merged
2010-11-26 nipkow 2010-11-26 new lemma
2010-11-26 wenzelm 2010-11-26 lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;
2010-11-26 wenzelm 2010-11-26 prefer non-classical eliminations in Pure reasoning, notably "rule" steps;
2010-11-26 wenzelm 2010-11-26 discontinued global "Isabelle" symlink, to make each distribution even more self-contained;
2010-11-26 wenzelm 2010-11-26 more correct spelling;
2010-11-26 haftmann 2010-11-26 globbing constant expressions use more idiomatic underscore rather than star
2010-11-26 haftmann 2010-11-26 globbing constant expressions use more idiomatic underscore rather than star; precised
2010-11-26 haftmann 2010-11-26 datatype constructor glob for code_reflect