isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip

save image as PNG or PDF;
2014-09-25, by wenzelm
support for PNG output;
2014-09-25, by wenzelm
more isatests (on lxbroy4);
2014-09-25, by wenzelm
document 'corec_transfer'
2014-09-25, by desharna
generate 'corec_transfer' for codatatypes
2014-09-25, by desharna
document 'rec_transfer'
2014-09-25, by desharna
generate 'rec_transfer' for datatypes
2014-09-25, by desharna
generate 'dtor_corec_transfer' for codatatypes
2014-09-25, by desharna
generate 'ctor_rec_transfer' for datatypes
2014-09-25, by desharna
goal generation for xtor_co_rec_transfer
2014-09-01, by traytel
commented out some tests that require external tools (e.g. ghc)
2014-09-25, by blanchet
added useful options to CVC4
2014-09-25, by blanchet
subscribe for isatest
2014-09-25, by traytel
even more deads go to the end (continuation of e3a01b73579f)
2014-09-25, by traytel
added function size1
2014-09-25, by nipkow
added lemmas
2014-09-24, by haftmann
tuned
2014-09-24, by haftmann
avoid type variable name clash
2014-09-24, by blanchet
tuning
2014-09-24, by blanchet
made N2M tests conditional, since they appear to cause Isatest timeouts and are kind of slow
2014-09-24, by blanchet
improved 'bnf' parser
2014-09-24, by blanchet
updated SMT certificates
2014-09-24, by blanchet
allow homogeneous nesting for SMT (co)datatypes
2014-09-24, by blanchet
interleave (co)datatypes in the right order w.r.t. dependencies
2014-09-24, by blanchet
rule out nested (co)recursion for SMT (co)datatypes
2014-09-24, by blanchet
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
2014-09-24, by blanchet
tuning
2014-09-24, by blanchet
simpler proof
2014-09-24, by blanchet
added nice standard syntax
2014-09-24, by nipkow
clarified timeout for isatest;
2014-09-22, by wenzelm
merged
2014-09-22, by wenzelm
discontinued old "xnum" token category;
2014-09-22, by wenzelm
added csdp-6.x for proof method (sos csdp);
2014-09-22, by wenzelm
examples for local CSDP executable;
2014-09-22, by wenzelm
clarified SOS tool setup vs. examples;
2014-09-22, by wenzelm
make 'set_induct0' tactic more robust w.r.t multiple arguments constructors
2014-09-22, by desharna
merged
2014-09-22, by wenzelm
clarified ISABELLE_POLYML;
2014-09-22, by wenzelm
drop workaround addressed by d0d3c30806b4
2014-09-22, by Andreas Lochbihler
renamed ISABELLE_POLYML to ML_SYSTEM_POLYML, to avoid overlap with ISABELLE_POLYML_PATH;
2014-09-21, by wenzelm
more standard Isabelle/ML operations;
2014-09-21, by wenzelm
tuned;
2014-09-21, by wenzelm
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-09-21, by haftmann
corrected slip in documentation
2014-09-21, by haftmann
Removed double space
2014-09-20, by steckerm
Changed proof method to auto for custom Waldmeister lemma
2014-09-20, by steckerm
Minor fixes in ATP_Waldmeister
2014-09-20, by steckerm
Made encoded type for apply less restrictive
2014-09-20, by steckerm
Updated fix_name function
2014-09-20, by steckerm
Added support for partial function application
2014-09-20, by steckerm
Improved equality handling in skolemization
2014-09-20, by steckerm
Re-added hypothesis argument to problem generation
2014-09-20, by steckerm
always annotate potentially polymorphic Haskell numerals
2014-09-18, by haftmann
tuned
2014-09-18, by haftmann
simplified and tuned using signed_string_of_int
2014-09-18, by haftmann
tuned data structure
2014-09-18, by haftmann
tuning
2014-09-19, by blanchet
documented limitations
2014-09-19, by blanchet
more honest 'primcorec' -- don't parse a theorem name that is then ignored
2014-09-19, by blanchet
tuning
2014-09-19, by blanchet

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip

isabelle