2010-12-06 bulwahn 2010-12-06 adding mutabelle as a component and an isabelle tool to be used in regression testing
2010-12-06 bulwahn 2010-12-06 commenting out sledgehammer_mtd in Mutabelle
2010-12-06 bulwahn 2010-12-06 removing declaration in quickcheck to really enable exhaustive testing
2010-12-06 bulwahn 2010-12-06 adding timeout to try invocation in mutabelle
2010-12-06 bulwahn 2010-12-06 adding filtering, sytactic welltyping, and sledgehammer method in mutabelle
2010-12-06 haftmann 2010-12-06 replace `type_mapper` by the more adequate `type_lifting`
2010-12-06 haftmann 2010-12-06 moved bootstrap of type_lifting to Fun
2010-12-06 haftmann 2010-12-06 replace `type_mapper` by the more adequate `type_lifting`
2010-12-06 wenzelm 2010-12-06 avoid explicit encoding -- acknowledge UTF-8 as global default and Isabelle/jEdit preference of UTF-8-Isabelle;
2010-12-05 wenzelm 2010-12-05 IsabelleText font: include Cyrillic, Hebrew, Arabic from DejaVu Sans 2.32;
2010-12-05 wenzelm 2010-12-05 command 'notepad' replaces former 'example_proof';
2010-12-05 wenzelm 2010-12-05 prefer 'notepad' over 'example_proof';
2010-12-05 haftmann 2010-12-05 merged
2010-12-04 haftmann 2010-12-04 more intimate definition of fold_list / fold_once in terms of fold
2010-12-04 haftmann 2010-12-04 canonical fold signature
2010-12-04 wenzelm 2010-12-04 formal notepad without any result;
2010-12-04 wenzelm 2010-12-04 added Syntax.default_root; simplified Syntax.parse operations; clarified treatment of syntax root for translation rules -- refrain from logical_type replacement; tuned error message;
2010-12-04 wenzelm 2010-12-04 eliminated obsolete Token.Malformed -- subsumed by Token.Error;
2010-12-04 wenzelm 2010-12-04 tuned @{datatype} using Syntax.pretty_priority (NB: postfix type application yields Syntax.max_pri, so arguments in prefix application require higher priority);
2010-12-04 wenzelm 2010-12-04 added Syntax.pretty_priority;
2010-12-03 haftmann 2010-12-03 merged
2010-12-03 haftmann 2010-12-03 conventional point-free characterization of rsp_fold
2010-12-03 haftmann 2010-12-03 replaced memb by existing List.member
2010-12-03 haftmann 2010-12-03 explicit type constraint; streamlined notation
2010-12-03 haftmann 2010-12-03 tuned proposition
2010-12-03 haftmann 2010-12-03 lemma multiset_of_rev
2010-12-03 haftmann 2010-12-03 lemmas fold_remove1_split and fold_multiset_equiv
2010-12-03 wenzelm 2010-12-03 minor tuning for release;
2010-12-03 wenzelm 2010-12-03 source files are always encoded as UTF-8;
2010-12-03 wenzelm 2010-12-03 eliminated fragile HTML.with_charset -- always use utf-8;
2010-12-03 wenzelm 2010-12-03 recoded latin1 as utf8; use textcomp for some text symbols where it appears appropriate;
2010-12-03 wenzelm 2010-12-03 removed old generated stuff; removed DOS line endings;
2010-12-03 wenzelm 2010-12-03 comment;
2010-12-03 blanchet 2010-12-03 update documentation
2010-12-03 blanchet 2010-12-03 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
2010-12-03 blanchet 2010-12-03 export more information about available SMT solvers
2010-12-03 wenzelm 2010-12-03 setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
2010-12-02 traytel 2010-12-02 use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."
2010-12-03 wenzelm 2010-12-03 updated generated file;
2010-12-03 wenzelm 2010-12-03 removed confusing comments (cf. 500171e7aa59);
2010-12-03 wenzelm 2010-12-03 merged
2010-12-03 haftmann 2010-12-03 removed outdated lint script
2010-12-03 blanchet 2010-12-03 merged
2010-12-03 blanchet 2010-12-03 compile
2010-12-03 blanchet 2010-12-03 run synchronous Auto Tools in parallel
2010-12-03 krauss 2010-12-03 really fixed comment (cf. 7abeb749ae99)
2010-12-03 huffman 2010-12-03 theorem names generated by the (rep_)datatype command now have mandatory qualifiers
2010-12-03 krauss 2010-12-03 eliminated unqualified accesses of datatype facts -- it seems like they all of them were unintended
2010-12-03 bulwahn 2010-12-03 NEWS
2010-12-03 bulwahn 2010-12-03 only instantiate type variable if there exists some in quickcheck
2010-12-03 bulwahn 2010-12-03 fixing comment in library
2010-12-03 bulwahn 2010-12-03 adapting predicate_compile_quickcheck
2010-12-03 bulwahn 2010-12-03 adding a nice definition of Id_on for quickcheck and nitpick
2010-12-03 bulwahn 2010-12-03 adding code equation for finiteness of finite types
2010-12-03 bulwahn 2010-12-03 improving sledgehammer_tactic and adding relevance filtering to the tactic
2010-12-03 bulwahn 2010-12-03 adapting mutabelle
2010-12-03 bulwahn 2010-12-03 adapting SML_Quickcheck to recent changes
2010-12-03 bulwahn 2010-12-03 explaining quickcheck testers in the documentation
2010-12-03 bulwahn 2010-12-03 adapting quickcheck examples
2010-12-03 bulwahn 2010-12-03 improving presentation of quickcheck reports