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

more tweaking of TPTP/CASC setup
2012-04-27, by blanchet
added a basic sanity check for quot_map
2012-04-26, by kuncar
tuned comment;
2012-04-26, by wenzelm
fixed bug in handling of new numerals -- the left-hand side of "Numeral1 = 1" should be left alone and not translated to a built-in Kodkod numeral in the specification of the "numeral" function
2012-04-26, by blanchet
merged
2012-04-26, by wenzelm
add code equation for real_of_float
2012-04-26, by hoelzl
tuned; don't generate abs code if quotient_type is used
2012-04-26, by kuncar
support Quotient map theorems with invariant parameters
2012-04-26, by kuncar
use a quot_map theorem attribute instead of the complicated map attribute
2012-04-26, by kuncar
further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
2012-04-26, by blanchet
put Satallax first, at least for now (useful for experiments)
2012-04-26, by blanchet
tuning
2012-04-26, by blanchet
tuning
2012-04-26, by blanchet
tentatively tag hypotheses as definition -- this sometimes help the "tptp_sledgehammer" tool (e.g. SEU466^1.p)
2012-04-26, by blanchet
tuning; no need for relevance filter
2012-04-26, by blanchet
tuning
2012-04-25, by blanchet
don't extensionalize formulas for higher-order provers -- Satallax in particular will only expand definitions of the form "constant = ..."
2012-04-25, by blanchet
don't use the native choice operator if the type encoding isn't higher-order
2012-04-25, by blanchet
tuning
2012-04-25, by blanchet
more work on TPTP Isabelle and Sledgehammer tactics
2012-04-25, by blanchet
more work on CASC setup
2012-04-25, by blanchet
more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
2012-04-25, by wenzelm
mingw is windows (still inactive);
2012-04-25, by wenzelm
add Caratheodories theorem for semi-rings of sets
2012-04-25, by hoelzl
moved lemmas to appropriate places
2012-04-25, by hoelzl
register polyml executables so that Cygwin rebaseall will see them;
2012-04-25, by wenzelm
merged
2012-04-25, by wenzelm
smarter PDF_VIEWER defaults, based on hints by Lars Noschinski;
2012-04-25, by wenzelm
equate positive Lebesgue integral and MV-Analysis' Gauge integral
2012-04-25, by hoelzl
correct lemma name
2012-04-25, by hoelzl
tweak TPTP Nitpick's output
2012-04-25, by blanchet
remove too aggressive skolemization optimization (prevented discovery of a model in SYN994^1)
2012-04-25, by blanchet
improve precision (noticed on SEV296^5.thy) -- the exception for "bool" used to be necessary because of a hack where "opt" meant two different things
2012-04-25, by blanchet
output SZS status as early as possible
2012-04-25, by blanchet
sorted lemma list in NEWS
2012-04-25, by hoelzl
merged
2012-04-25, by wenzelm
reactivated ListCellRenderer for Java 6 (cf. b9e2ed4b1579, 0ddac15782e4, de249b5ae6e2);
2012-04-25, by wenzelm
enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
2012-04-25, by wenzelm
updated README;
2012-04-25, by wenzelm
include generated application wrapper;
2012-04-25, by wenzelm
back to mature jdk1.6.0_31, to avoid issues like Sidekick TAB completion and generic ListCellRenderer;
2012-04-25, by wenzelm
ISABELLE_JDK_HOME is already provided by isatest shell environment;
2012-04-25, by wenzelm
added splash screen, to reduce confusion when waiting for main application to start up;
2012-04-25, by wenzelm
move polyml within Cygwin /usr/local to simplify its rebasing;
2012-04-25, by wenzelm
improved spelling;
2012-04-25, by wenzelm
added "no_atp"s for extremely prolific, useless facts for ATPs
2012-04-25, by blanchet
tuned;
2012-04-24, by wenzelm
merged
2012-04-24, by wenzelm
made "split_last" more robust in the face of obscure low-level errors
2012-04-24, by blanchet
removed confusing error
2012-04-24, by blanchet
some friendly message;
2012-04-24, by wenzelm
merged
2012-04-24, by wenzelm
merged
2012-04-24, by wenzelm
merged
2012-04-24, by sultana
merged
2012-04-24, by sultana
reversed Tools to Actions Mirabelle renaming;
2012-04-24, by sultana
tuned;
2012-04-24, by sultana
reintroduce file offsets in Mirabelle output, but make sure they are not influenced by the length of the path
2012-04-24, by blanchet
doc update
2012-04-24, by nipkow
prefer evince over old xpdf -- NB: x86-cygwin bundles its own application;
2012-04-24, by wenzelm

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

isabelle