isabelle: Graph

Library/Fraction_Field.thy: ordering relations for fractions
2010-04-24, by huffman
renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
2010-04-25, by wenzelm
more systematic treatment of data -- avoid slightly odd nested tuples here;
2010-04-25, by wenzelm
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
2010-04-25, by wenzelm
misc tuning and simplification;
2010-04-25, by wenzelm
simplified some private bindings;
2010-04-25, by wenzelm
classrel and arity completion by krauss/schropp;
2010-04-25, by wenzelm
removed obsolete/unused Proof.match_bind;
2010-04-25, by wenzelm
modernized naming conventions of main Isar proof elements;
2010-04-25, by wenzelm
goals: simplified handling of implicit variables -- removed obsolete warning;
2010-04-25, by wenzelm
updated generated files;
2010-04-23, by wenzelm
cover 'schematic_lemma' etc.;
2010-04-23, by wenzelm
mark schematic statements explicitly;
2010-04-23, by wenzelm
eliminated spurious schematic statements;
2010-04-23, by wenzelm
explicit 'schematic_theorem' etc. for schematic theorem statements;
2010-04-23, by wenzelm
collapse category "schematic goal" in keyword table -- Proof General does not know about this;
2010-04-23, by wenzelm
added keyword category "schematic goal", which prevents any attempt to fork the proof;
2010-04-23, by wenzelm
merged
2010-04-23, by wenzelm
merged
2010-04-23, by haftmann
separated instantiation of division_by_zero
2010-04-23, by haftmann
epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance
2010-04-23, by haftmann
adapted to new times_divide_eq simp situation
2010-04-23, by haftmann
epheremal replacement of field_simps by field_eq_simps
2010-04-23, by haftmann
dequalified fact name
2010-04-23, by haftmann
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
2010-04-23, by haftmann
separated instantiation of division_by_zero
2010-04-23, by haftmann
dequalified fact name
2010-04-23, by haftmann
less special treatment of times_divide_eq [simp]
2010-04-23, by haftmann
sharpened constraint (c.f. 4e7f5b22dd7d)
2010-04-23, by haftmann
more localization; tuned proofs
2010-04-23, by haftmann
more localization; factored out lemmas for division_ring
2010-04-23, by haftmann
modernized abstract algebra theories
2010-04-23, by haftmann
merged
2010-04-23, by haftmann
swapped generic code generator and SML code generator
2010-04-22, by haftmann
removed obsolete Named_Thm_Set -- Named_Thms provides efficient member operation;
2010-04-23, by wenzelm
Item_Net/Named_Thms: export efficient member operation;
2010-04-23, by wenzelm
initialized atps reference with standard setup in the atp manager
2010-04-23, by bulwahn
compile
2010-04-23, by blanchet
handle SPASS's equality predicate correctly in Isar proof reconstruction
2010-04-23, by blanchet
merged
2010-04-23, by blanchet
added Isar proof reconstruction support for SPASS -- which means all provers can now yield Isar proofs;
2010-04-23, by blanchet
remove hack that is no longer necessary now that "ATP_Wrapper" properly detects which ATPs are installed
2010-04-22, by blanchet
set "atps" reference's default value to "(remote_)e (remote_)spass (remote_)vampire", based on what is installed
2010-04-22, by blanchet
minor code cleanup
2010-04-22, by blanchet
if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
2010-04-22, by blanchet
"remote_e" and "remote_vampire" support TSTP proof output + fix "overlord" mode ATP output postprocessing
2010-04-22, by blanchet
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