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 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip

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 more | (0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle