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

Simplifying the labels in the proof of the SMT solver veriT.
2014-07-30, by fleury
Changing ~ into - for unuary minus (not supported by veriT)
2014-07-30, by fleury
imported patch satallax_skolemization_in_tree_part
2014-07-30, by fleury
imported patch hilbert_choice_support
2014-07-30, by fleury
veriT changes for lifted terms, and ite_elim rules.
2014-07-30, by fleury
imported patch satallax_proof_support_Sledgehammer
2014-07-30, by fleury
Basic support for the higher-order ATP Satallax.
2014-07-30, by fleury
Subproofs for the SMT solver veriT.
2014-07-30, by fleury
Basic support for the SMT prover veriT.
2014-07-30, by fleury
removing the '= True' generated by Leo-II.
2014-07-30, by fleury
Skolemization support for leo-II and Zipperposition.
2014-07-30, by fleury
document property 'set_induct'
2014-07-30, by desharna
generate 'set_induct' theorem for codatatypes
2014-07-30, by desharna
also try 'metis' with 'full_types'
2014-07-30, by blanchet
header tuning
2014-07-29, by blanchet
correctly translate THF functions from terms to types
2014-07-28, by blanchet
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
2014-07-27, by blanchet
back to post-release mode -- after fork point;
2014-07-27, by wenzelm
tuned;
2014-07-27, by wenzelm
tuned;
2014-07-27, by wenzelm
no -optimise -- produces bad bytecode;
2014-07-26, by wenzelm
output state first -- avoid fluctuation wrt. warnings, errors, etc.;
2014-07-26, by wenzelm
tuned comment;
2014-07-25, by wenzelm
updated to polyml-5.5.2-1 which addresses two hard crashes;
2014-07-25, by wenzelm
updated to cygwin-20140725, which is presumably close to Cygwin 1.7.31-1;
2014-07-25, by wenzelm
added more functions and lemmas
2014-07-25, by nipkow
proper mkdir;
2014-07-25, by wenzelm
proper option -O;
2014-07-25, by wenzelm
some reshuffling of Poly/ML version to evade failing tests;
2014-07-25, by wenzelm
old 'defs' is legacy --- slightly odd side-entry that bypasses regular Local_Theory.define interface;
2014-07-25, by wenzelm
proper volume name, such that background image is found in /Volumes/Isabelle/.background;
2014-07-25, by wenzelm
tuned;
2014-07-25, by wenzelm
tuned message;
2014-07-25, by wenzelm
setup for drag-and-drop DMG;
2014-07-25, by wenzelm
merge
2014-07-25, by blanchet
reordered provers
2014-07-25, by blanchet
compile
2014-07-25, by blanchet
faster minimization by not adding facts that are already in the simpset
2014-07-25, by blanchet
added missing facts to proof method
2014-07-25, by blanchet
don't lose 'minimize' flag before it reaches Isar proof text generation
2014-07-25, by blanchet
tuning
2014-07-25, by blanchet
avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
2014-07-25, by blanchet
compile
2014-07-25, by blanchet
more robustness in Isar proof construction
2014-07-25, by blanchet
tuning
2014-07-25, by blanchet
merged
2014-07-24, by wenzelm
more elementary exception handling: evade hard crash of (Runtime.thread true undefined) on Poly/ML 5.5.1 and 5.5.2;
2014-07-24, by wenzelm
tuned code
2014-07-24, by blanchet
having extra assumptions (typically from a context) means there is no chance to have a valid code equation => skip decoding and registration of the code equations
2014-07-24, by kuncar
store explicitly quotient types with no_code => more precise registration of code equations
2014-07-24, by kuncar
don't needlessly regenerate entire file when the time stamps are equal
2014-07-24, by blanchet
eliminated source of 'DUP's in MaSh
2014-07-24, by blanchet
fixed sorting (broken since 9cc802a8ab06)
2014-07-24, by blanchet
reenabled MaSh for Isabelle2014 release (hopefully)
2014-07-24, by blanchet
beware of duplicate fact names
2014-07-24, by blanchet
refined filter for ATP steps to avoid 'have True' steps in E proofs
2014-07-24, by blanchet
filter out 'theory(...)' from dependencies early on
2014-07-24, by blanchet
introduce fact chaining also under first step
2014-07-24, by blanchet
'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)
2014-07-24, by blanchet
merged
2014-07-24, by wenzelm

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

isabelle