2014-09-24 blanchet 2014-09-24 rule out nested (co)recursion for SMT (co)datatypes
2014-09-24 blanchet 2014-09-24 gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
2014-09-24 blanchet 2014-09-24 tuning
2014-09-24 blanchet 2014-09-24 simpler proof
2014-09-24 nipkow 2014-09-24 added nice standard syntax
2014-09-22 wenzelm 2014-09-22 clarified timeout for isatest;
2014-09-22 wenzelm 2014-09-22 merged
2014-09-22 wenzelm 2014-09-22 discontinued old "xnum" token category; simplified Lexicon.read_num, Lexicon.read_float: no sign here; express ZF numerals via "num" with mixfix grammar; recovered printing of ZF numerals: "one" is abbreviation;
2014-09-22 wenzelm 2014-09-22 added csdp-6.x for proof method (sos csdp);
2014-09-22 wenzelm 2014-09-22 examples for local CSDP executable;
2014-09-22 wenzelm 2014-09-22 clarified SOS tool setup vs. examples;
2014-09-22 desharna 2014-09-22 make 'set_induct0' tactic more robust w.r.t multiple arguments constructors
2014-09-22 wenzelm 2014-09-22 merged
2014-09-22 wenzelm 2014-09-22 clarified ISABELLE_POLYML; added some isatests -- ISABELLE_SCALA still inactive due to problems with case-insensible file-system;
2014-09-22 Andreas Lochbihler 2014-09-22 drop workaround addressed by d0d3c30806b4
2014-09-21 wenzelm 2014-09-21 renamed ISABELLE_POLYML to ML_SYSTEM_POLYML, to avoid overlap with ISABELLE_POLYML_PATH;
2014-09-21 wenzelm 2014-09-21 more standard Isabelle/ML operations;
2014-09-21 wenzelm 2014-09-21 tuned;
2014-09-21 haftmann 2014-09-21 explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-09-21 haftmann 2014-09-21 corrected slip in documentation
2014-09-20 steckerm 2014-09-20 Removed double space
2014-09-20 steckerm 2014-09-20 Changed proof method to auto for custom Waldmeister lemma
2014-09-20 steckerm 2014-09-20 Minor fixes in ATP_Waldmeister
2014-09-20 steckerm 2014-09-20 Made encoded type for apply less restrictive
2014-09-20 steckerm 2014-09-20 Updated fix_name function
2014-09-20 steckerm 2014-09-20 Added support for partial function application
2014-09-20 steckerm 2014-09-20 Improved equality handling in skolemization
2014-09-20 steckerm 2014-09-20 Re-added hypothesis argument to problem generation
2014-09-18 haftmann 2014-09-18 always annotate potentially polymorphic Haskell numerals
2014-09-18 haftmann 2014-09-18 tuned
2014-09-18 haftmann 2014-09-18 simplified and tuned using signed_string_of_int
2014-09-18 haftmann 2014-09-18 tuned data structure
2014-09-19 blanchet 2014-09-19 tuning
2014-09-19 blanchet 2014-09-19 documented limitations
2014-09-19 blanchet 2014-09-19 more honest 'primcorec' -- don't parse a theorem name that is then ignored
2014-09-19 blanchet 2014-09-19 tuning
2014-09-19 blanchet 2014-09-19 added a few tests for 'old_datatype'
2014-09-19 blanchet 2014-09-19 reintroduced old setup for size of basic types
2014-09-19 blanchet 2014-09-19 keep obsolete interpretations in Main, to avoid merge trouble
2014-09-19 blanchet 2014-09-19 made new 'primrec' bootstrapping-capable
2014-09-19 blanchet 2014-09-19 tuning
2014-09-19 blanchet 2014-09-19 tuning
2014-09-19 traytel 2014-09-19 typo
2014-09-19 traytel 2014-09-19 regression tests for n2m
2014-09-19 Andreas Lochbihler 2014-09-19 merged
2014-09-18 Andreas Lochbihler 2014-09-18 add lemma
2014-09-18 blanchet 2014-09-18 tuned imports
2014-09-18 blanchet 2014-09-18 removed debugging junk
2014-09-18 blanchet 2014-09-18 help AFP entry 'Free-Groups' to compile
2014-09-18 blanchet 2014-09-18 reintroduced an instantiation of 'size' for 'numerals'
2014-09-18 blanchet 2014-09-18 use selector
2014-09-18 blanchet 2014-09-18 moved old 'size' generator together with 'old_datatype'
2014-09-18 blanchet 2014-09-18 moved datatype realizer to 'old_datatype' and colleagues
2014-09-18 blanchet 2014-09-18 careful with op = in n2m (actually by Dmitriy Traytel)
2014-09-18 blanchet 2014-09-18 fixed attribute name in docs (thanks to Andreas Lochbihler)
2014-09-18 blanchet 2014-09-18 updated NEWS
2014-09-18 blanchet 2014-09-18 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer) * * * made example compile again
2014-09-18 blanchet 2014-09-18 increased 'HOL-Proofs' timeout
2014-09-18 blanchet 2014-09-18 made 'mk_pointfree' work again in local theories
2014-09-18 blanchet 2014-09-18 fixed authorship