isabelle: Graph

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
some actual workaround to remove document nodes;
2014-07-28, by wenzelm
Added tag Isabelle2014-RC1 for changeset c0fd03d13d28
2014-07-27, by wenzelm
tuned;
2014-08-09, by wenzelm
tuned
2014-08-09, by nipkow
add complete_lattice instances for Enum.finite_* types such that quickcheck deals with lattice class operations
2014-08-08, by Andreas Lochbihler
tuned
2014-08-08, by nipkow
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
2014-08-07, by blanchet
generate nicer 'set' theorems for (co)datatypes
2014-08-07, by blanchet
compile
2014-08-07, by blanchet
took out test driver
2014-08-07, by blanchet
make TPTP tools work on polymorphic (TFF1) problems as well
2014-08-07, by blanchet
put comments between TPTP lines to comply with TPTP BNF
2014-08-07, by blanchet
test driver
2014-08-07, by blanchet
treat variables as frees in 'conjecture's
2014-08-07, by blanchet
support TFF1 in TPTP parser/interpreter
2014-08-07, by blanchet
tuning
2014-08-07, by blanchet
tuned
2014-08-07, by traytel
tuned
2014-08-07, by nipkow
tuned
2014-08-07, by nipkow
merged
2014-08-06, by traytel
handle deep nesting in N2M
2014-08-06, by traytel
made tactic more robust
2014-08-06, by traytel
added lemma
2014-08-06, by nipkow
replaced misleading - by _
2014-08-06, by nipkow
more correct clique computation for N2M
2014-08-05, by blanchet
regenerated ML-Lex/Yacc files
2014-08-05, by blanchet
correctly interpret arithmetic types
2014-08-05, by blanchet
added 'datatype_compat' tests
2014-08-05, by blanchet
tuning whitespace
2014-08-05, by blanchet
tuned skolemization
2014-08-05, by blanchet
rationalize Skolem names
2014-08-05, by blanchet
tuning
2014-08-05, by blanchet
tuned code
2014-08-05, by blanchet
don't rename variables which will be renamed later anyway
2014-08-05, by blanchet
normalize skolem argument variable names so that they coincide when taking the conjunction
2014-08-05, by blanchet
tuning
2014-08-05, by blanchet
tuned comments
2014-08-04, by blanchet
deal with E definitions
2014-08-04, by blanchet
updated 'compress' docs
2014-08-04, by blanchet
cleaner 'compress' option
2014-08-04, by blanchet
renamed 'sh_minimize' to 'minimize'; compile;
2014-08-04, by blanchet
restored more sorting
2014-08-04, by blanchet
tuned terminology (cf. 'isar_proofs' option)
2014-08-04, by blanchet
sort facts in minimizer as well
2014-08-04, by blanchet
default on 'metis' for ATPs if preplaying is disabled
2014-08-04, by blanchet
more informative preplay failures
2014-08-04, by blanchet
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
2014-08-04, by blanchet
slightly earlier exit from preplaying
2014-08-04, by blanchet
honor 'dont_minimize' option when preplaying one-liner proof
2014-08-04, by blanchet
Metis is being used to emulate E steps;
2014-06-22, by sultana
updated application of print_tac to take context parameter;
2014-06-22, by sultana
better duplicate detection
2014-08-02, by blanchet
normalize conjectures vs. negated conjectures when comparing terms
2014-08-01, by blanchet
tweaked 'clone' formula detection
2014-08-01, by blanchet
fine-tuned Isar reconstruction, esp. boolean simplifications
2014-08-01, by blanchet
centralized boolean simplification so that e.g. LEO-II benefits from it
2014-08-01, by blanchet
careful when compressing 'obtains'
2014-08-01, by blanchet
better handling of variable names
2014-08-01, by blanchet
try to get rid of skolems first
2014-08-01, by blanchet
nicer generated variable names
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
no need to 'obtain' variables not in formula
2014-08-01, by blanchet
more precise handling of LEO-II skolemization
2014-08-01, by blanchet
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
peek instead of joining -- is perhaps less risky
2014-08-01, by blanchet
export ML function
2014-08-01, by blanchet
compile
2014-08-01, by blanchet
removed 'metisFT' support in Mirabelle
2014-08-01, by blanchet
removed Mirabelle minimization code
2014-08-01, by blanchet
modernized Mirabelle (a bit) and made it compile
2014-08-01, by blanchet
restored a bit of laziness
2014-08-01, by blanchet
reorder quantifiers to ease Z3 skolemization
2014-08-01, by blanchet
tuned order of arguments
2014-08-01, by blanchet
tuned name context code
2014-08-01, by blanchet
tuned whitespace
2014-08-01, by blanchet
more rational unskolemizing of names
2014-08-01, by blanchet
added appropriate method for skolemization of Z3 steps to the mix
2014-08-01, by blanchet
pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)
2014-08-01, by blanchet
honor 'try0' also for one-liners
2014-08-01, by blanchet
tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence
2014-08-01, by blanchet
further minimize one-liner
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
eliminated needlessly complex message tail
2014-08-01, by blanchet
updated NEWS
2014-08-01, by blanchet
update documentation after removal of 'min' subcommand
2014-08-01, by blanchet
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
2014-08-01, by blanchet
rationalized preplaying by eliminating (now superfluous) laziness
2014-08-01, by blanchet
removed proof methods as provers from docs
2014-08-01, by blanchet
simplified minimization logic
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
remove lambda-lifting related assumptions from generated Isar proofs
2014-08-01, by blanchet
whitespace tuning
2014-08-01, by blanchet
remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
2014-08-01, by blanchet
generate backquotes without markup, since this confuses preplay; bump up spying version identifier;
2014-08-01, by blanchet
simplified tactics slightly
2014-07-31, by traytel
cascading timeout in parallel evaluation, to rapidly find optimum
2014-07-31, by blanchet
put faster proof methods first
2014-07-30, by blanchet
use parallel preplay machinery also for one-line proofs
2014-07-30, by blanchet
updated docs
2014-07-30, by blanchet
always minimize Sledgehammer results by default
2014-07-30, by blanchet
tuned ML function name
2014-07-30, by blanchet
reduced preplay timeout to 1 s
2014-07-30, by blanchet
added more proof methods for one-liners
2014-07-30, by blanchet
unlift before uncombine, because the definition of a lambda-lifted symbol might have an SK combinator in it (in hybrid encodings)
2014-07-30, by blanchet
Improving robustness and indentation corrections.
2014-07-30, by fleury
Skolemization for tmp_ite_elim rule in the SMT solver veriT.
2014-07-30, by fleury
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
2014-07-30, by fleury
Whitespace and indentation correction.
2014-07-30, by fleury
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
proper perl;
2014-07-24, by wenzelm
less warnings -- ignore potential prover startup/shutdown races;
2014-07-24, by wenzelm
tuned spelling;
2014-07-24, by wenzelm
further distinction of Isabelle distribution: alert for identified release candidates;
2014-07-24, by wenzelm
updated to scala-2.11.2;
2014-07-24, by wenzelm
clarified file names;
2014-07-24, by wenzelm
less ambitious isatest, avoid "Exception- InternalError: Backing up too far (32bit) raised while compiling" in polyml-5.4.1;
2014-07-24, by wenzelm
tuned imports;
2014-07-24, by wenzelm
proper scope of comments;
2014-07-24, by wenzelm
make SML/NJ happy;
2014-07-24, by wenzelm
prevent beta-contraction in proving extra assumptions for abs_eq
2014-07-24, by kuncar
more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
2014-07-24, by wenzelm
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
2014-07-24, by wenzelm
tuned;
2014-07-24, by wenzelm
less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
2014-07-24, by wenzelm
updated NEWS according to d38a98f496dd (see also bdc2c6b40bf2);
2014-07-24, by wenzelm
stick to external proofs when invoking E, because they are more detailed and do not merge steps
2014-07-24, by blanchet
more robust handling of types for skolems (modeled as Frees)
2014-07-24, by blanchet
tuning
2014-07-24, by blanchet
repaired named derivations
2014-07-24, by blanchet
use the noted theorems in 'BNF_Comp'
2014-07-24, by blanchet
use the noted theorem whenever possible, also in 'BNF_Def'
2014-07-24, by blanchet
use termtab instead of (perhaps overly sensitive) thmtab
2014-07-24, by blanchet
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
2014-07-24, by blanchet
tuned message;
2014-07-23, by wenzelm
added action "isabelle.options" (despite problems with initial window size);
2014-07-23, by wenzelm
more official Thy_Info.script_thy;
2014-07-23, by wenzelm
more frugal edits;
2014-07-23, by wenzelm
enable hires explictly, as seen for other high-end Java applications on the Web;
2014-07-23, by wenzelm
more markup;
2014-07-23, by wenzelm
another attempt at more aggressive auto-loading (amending af28fdd50690) -- hidden buffers are now suppressed;
2014-07-23, by wenzelm
more frugal edits;
2014-07-23, by wenzelm
more explicit treatment of cleared nodes (removal is implicit);
2014-07-23, by wenzelm
clarified display;
2014-07-23, by wenzelm
more workarounds for scalac;
2014-07-23, by wenzelm
clarified display;
2014-07-23, by wenzelm
avoid redundant data structure;
2014-07-23, by wenzelm
more explicit discrimination of empty nodes -- suppress from Theories panel;
2014-07-23, by wenzelm
tuned;
2014-07-23, by wenzelm
tuned comments;
2014-07-23, by wenzelm
clarified module name: facilitate alternative GUI frameworks;
2014-07-23, by wenzelm
proper change of perspective for removed nodes (stemming from closed buffers);
2014-07-23, by wenzelm
tuned signature;
2014-07-23, by wenzelm
some robustification of console output;
2014-07-22, by wenzelm
updated ErrorList.jar;
2014-07-22, by wenzelm
discontinued presumable workarounds for extra inter-theory space, which are obsolete since 0e5fa27d3293;
2014-07-22, by wenzelm
evade problems with MikTeX on Windows;
2014-07-22, by wenzelm
tuned messages;
2014-07-22, by wenzelm
support multiple selected print operations instead of slightly odd "menu";
2014-07-22, by wenzelm
more default imports;
2014-07-22, by wenzelm
no keyword completion within word context -- especially avoid its odd visual rendering;
2014-07-22, by wenzelm
merged
2014-07-22, by Andreas Lochbihler
merged
2014-07-21, by Andreas Lochbihler
add parametricity lemmas
2014-07-21, by Andreas Lochbihler
add lemma
2014-07-21, by Andreas Lochbihler
merged
2014-07-21, by wenzelm
refer to Simplifier Trace panel on first invocation;
2014-07-21, by wenzelm
removed unused markup (cf. 2f7d91242b99);
2014-07-21, by wenzelm
regular message to refer to Simplifier Trace panel (unused);
2014-07-21, by wenzelm
proper Swing buttons instead of active areas within text (by Lars Hupel);
2014-07-21, by wenzelm
misc tuning and simplification;
2014-07-21, by wenzelm
clarified "simp_trace_new" and corresponding isar-ref section;
2014-07-21, by wenzelm
more on "Simplifier trace" (by Lars Hupel);
2014-07-21, by wenzelm
always complete explicit symbols;
2014-07-21, by wenzelm
discontinued unfinished attempts at syntactic word context (see 2e1398b484aa, 08a1c860bc12, 7f229b0212fe) -- back to more basic completion of Isabelle2013-2;
2014-07-21, by wenzelm
updated to jdk-7u65;
2014-07-21, by wenzelm
regression test for datatypes defined in IsaFoR
2014-07-21, by traytel
ghc mac installation repaired; test back on.
2014-07-21, by kleing
proper condition wrt. ISABELLE_GHC (cf. 8840fa17e17c);
2014-07-20, by wenzelm