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 +30000 tip

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
by default, don't try to start ATPs that aren't installed
2010-04-16, by blanchet
fiddle with Sledgehammer option syntax
2010-04-16, by blanchet
added timestamp to proof
2010-04-16, by blanchet
restore order of clauses in TPTP output;
2010-04-16, by blanchet
optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
2010-04-16, by blanchet
output total time taken by Sledgehammer if "verbose" is set
2010-04-16, by blanchet
Sledgehammer: the empty set of fact () should mean nothing, not unchanged
2010-04-16, by blanchet
reorganize Sledgehammer's relevance filter slightly
2010-04-16, by blanchet
tell the user that Sledgehammer kills its siblings
2010-04-16, by blanchet
updated keywords;
2010-04-16, by wenzelm
replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix);
2010-04-16, by wenzelm
keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
2010-04-16, by wenzelm
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
2010-04-16, by wenzelm
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-04-16, by wenzelm
allow syntax types within abbreviations;
2010-04-16, by wenzelm
modernized old-style type abbreviations;
2010-04-16, by wenzelm
modernized type abbreviations;
2010-04-16, by wenzelm
local type abbreviations;
2010-04-16, by wenzelm
merged
2010-04-16, by blanchet
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
2010-04-16, by blanchet
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
2010-04-16, by blanchet
give more sensible names to "fol_type" constructors, as requested by a FIXME comment
2010-04-15, by blanchet
make Sledgehammer's output more debugging friendly
2010-04-15, by blanchet
made SML/NJ happy;
2010-04-16, by wenzelm
proper masking of dummy name_space;
2010-04-16, by wenzelm
salvaged some ML functors from decay, which is the natural consequence of lack of formal checking;
2010-04-16, by wenzelm
proper checking of ML functors (in Poly/ML 5.2 or later);
2010-04-16, by wenzelm

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

isabelle