isabelle: Graph

Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
2010-04-22, by blanchet
postprocess ATP output in "overlord" mode to make it more readable
2010-04-22, by blanchet
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short one-liner proof -- but in "debug" mode we do want to know what the exception is
2010-04-21, by blanchet
generate command-line in addition to timestamp in ATP output file, for debugging purposes
2010-04-21, by blanchet
pass relevant options from "sledgehammer" to "sledgehammer minimize";
2010-04-21, by blanchet
Finite set theory
2010-04-23, by Cezary Kaliszyk
merged
2010-04-22, by wenzelm
Tidied up using s/l
2010-04-22, by paulson
split Class.thy into parts to conserve a bit of memory and increase the chance of making it work on Cygwin with only 2 GB available;
2010-04-22, by wenzelm
fun_rel introduction and list_rel elimination for quotient package
2010-04-22, by Cezary Kaliszyk
lemmas concerning remdups
2010-04-22, by haftmann
lemma dlist_ext
2010-04-22, by haftmann
merged
2010-04-21, by haftmann
optionally ignore errors during translation of equations; tuned representation of abstraction points
2010-04-21, by haftmann
optionally ignore errors during translation of equations
2010-04-21, by haftmann
tolerate eta-variants in f_graph.cases (from inductive package); added test case;
2010-04-21, by krauss
simplified example
2010-04-21, by krauss
use only one thread in "Manual_Nits";
2010-04-21, by blanchet
merged
2010-04-21, by blanchet
clarify error message
2010-04-21, by blanchet
distinguish between the different ATP errors in the user interface;
2010-04-21, by blanchet
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
2010-04-21, by blanchet
use "Proof.goal" in Sledgehammer's minimizer (just like everywhere else in Sledgehammer), not "Proof.raw_goal"
2010-04-20, by blanchet
merged
2010-04-21, by bulwahn
make profiling depend on reference Quickcheck.timing
2010-04-21, by bulwahn
added examples for detecting switches
2010-04-21, by bulwahn
adopting documentation of the predicate compiler
2010-04-21, by bulwahn
removing dead code; clarifying function names; removing clone
2010-04-21, by bulwahn
adopting examples to changes in the predicate compiler
2010-04-21, by bulwahn
adopting quickcheck
2010-04-21, by bulwahn
tuning mutabelle; adding output of mutant theoryfile for interactive evaluation
2010-04-21, by bulwahn
added switch detection to the predicate compiler
2010-04-21, by bulwahn
added further inlining of boolean constants to the predicate compiler
2010-04-21, by bulwahn
adding more profiling to the predicate compiler
2010-04-21, by bulwahn
only add relevant predicates to the list of extra modes
2010-04-21, by bulwahn
switched off no_topmost_reordering
2010-04-21, by bulwahn
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
2010-04-21, by bulwahn
added option for specialisation to the predicate compiler
2010-04-21, by bulwahn
prefer functional modes of functions in the mode analysis
2010-04-21, by bulwahn
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
2010-04-21, by bulwahn
merged
2010-04-21, by hoelzl
Only use provided SMT-certificates in HOL-Multivariate_Analysis.
2010-04-21, by hoelzl
Translated remaining theorems about integration from HOL light.
2010-04-20, by himmelma
marked cygwin-poly as "e" test, which means further stages do not depend on it (website etc.);
2010-04-21, by wenzelm
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
2010-04-20, by huffman
Remove garbage.
2010-04-20, by ballarin
Remove garbage.
2010-04-20, by ballarin
recovered isabelle java, which was broken in ebfa4bb0d50f;
2010-04-20, by wenzelm
fix bug in SPASS's DFG output files, where "tc_bool" wasn't declared;
2010-04-20, by blanchet
merged
2010-04-20, by blanchet
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
2010-04-20, by blanchet
merge
2010-04-20, by blanchet
cosmetics
2010-04-19, by blanchet
don't redo an axiom selection in the first round of Sledgehammer "minimize"!;
2010-04-19, by blanchet
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
2010-04-19, by blanchet
added warning about inconsistent context to Metis;
2010-04-19, by blanchet
workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in "proof" is not highlighted
2010-04-19, by blanchet
got rid of somewhat pointless "pairname" function in Sledgehammer
2010-04-19, by blanchet
make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems
2010-04-19, by blanchet
cosmetics
2010-04-19, by blanchet
cosmetics
2010-04-19, by blanchet
cosmetics
2010-04-19, by blanchet
make Sledgehammer's minimizer also minimize Isar proofs
2010-04-19, by blanchet
don't use readable names if proof reconstruction is needed, because it uses the structure of names
2010-04-19, by blanchet
allow "_" in TPTP names in debug mode
2010-04-19, by blanchet
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
2010-04-19, by blanchet
set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
2010-04-19, by blanchet
get rid of "List.foldl" + add timestamp to SPASS
2010-04-19, by blanchet
less ambitious settings for cygwin-poly;
2010-04-20, by wenzelm
respectfullness and preservation of map for identity quotients
2010-04-20, by Cezary Kaliszyk
respectfullness and preservation of function composition
2010-04-20, by Cezary Kaliszyk
eta-normalize the goal since the original theorem is atomized
2010-04-20, by Cezary Kaliszyk
accept x86_64 results gracefully -- NB: Mac OS does report that if booted in 64 bit mode;
2010-04-20, by wenzelm
refer to THIS_JAVA dynamically, and treat ISABELLE_JAVA as static default -- relevant for nested JVM invocation within an existing Isabelle enviroment;
2010-04-20, by wenzelm
merged
2010-04-20, by haftmann
more appropriate representation of valid positions for abstractors
2010-04-19, by haftmann
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
2010-04-19, by haftmann
update_syntax: add new productions only once, to allow repeated local notation, for example;
2010-04-19, by wenzelm
tuned;
2010-04-19, by wenzelm
more platform information;
2010-04-19, by wenzelm
check JVM platform at most once -- still non-strict to prevent potential failure during initialization of object Platform;
2010-04-19, by wenzelm
some updates on multi-platform support;
2010-04-19, by wenzelm
merged
2010-04-19, by haftmann
explicit check sorts in abstract certificates; abstractor is part of dependencies
2010-04-19, by haftmann
polyml-platform script is superseded by ISABELLE_PLATFORM;
2010-04-19, by wenzelm
less ambitious settings for cygwin-poly;
2010-04-19, by wenzelm
merged
2010-04-19, by haftmann
more convenient equations for zip
2010-04-19, by haftmann
more platform info;
2010-04-17, by wenzelm
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
2010-04-17, by wenzelm
system properties determine the JVM platform, not the Isabelle one;
2010-04-17, by wenzelm
THIS_CYGWIN;
2010-04-17, by wenzelm
improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;
2010-04-17, by wenzelm
isatest: more robust treatment of remote files, less reliance on mounted file system;
2010-04-17, by wenzelm
merged
2010-04-17, by blanchet
added missing \n in output
2010-04-17, by blanchet