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

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
added a few tests for 'old_datatype'
2014-09-19, by blanchet
reintroduced old setup for size of basic types
2014-09-19, by blanchet
keep obsolete interpretations in Main, to avoid merge trouble
2014-09-19, by blanchet
made new 'primrec' bootstrapping-capable
2014-09-19, by blanchet
tuning
2014-09-19, by blanchet
tuning
2014-09-19, by blanchet
typo
2014-09-19, by traytel
regression tests for n2m
2014-09-19, by traytel
merged
2014-09-19, by Andreas Lochbihler
add lemma
2014-09-18, by Andreas Lochbihler
tuned imports
2014-09-18, by blanchet
removed debugging junk
2014-09-18, by blanchet
help AFP entry 'Free-Groups' to compile
2014-09-18, by blanchet
reintroduced an instantiation of 'size' for 'numerals'
2014-09-18, by blanchet
use selector
2014-09-18, by blanchet
moved old 'size' generator together with 'old_datatype'
2014-09-18, by blanchet
moved datatype realizer to 'old_datatype' and colleagues
2014-09-18, by blanchet
careful with op = in n2m (actually by Dmitriy Traytel)
2014-09-18, by blanchet
fixed attribute name in docs (thanks to Andreas Lochbihler)
2014-09-18, by blanchet
updated NEWS
2014-09-18, by blanchet
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
2014-09-18, by blanchet
increased 'HOL-Proofs' timeout
2014-09-18, by blanchet
made 'mk_pointfree' work again in local theories
2014-09-18, by blanchet
fixed authorship
2014-09-18, by blanchet
product over monoids for lists
2014-09-18, by haftmann
renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
2014-09-18, by blanchet
more meaningful record tests
2014-09-18, by blanchet
updated SMT certificates
2014-09-18, by blanchet
tuning
2014-09-17, by blanchet
take out selectors for records -- for derived records, these don't quite have the right type
2014-09-17, by blanchet
register Isabelle selectors as SMT selectors when possible
2014-09-17, by blanchet
added codatatype support for CVC4
2014-09-17, by blanchet

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

isabelle