isabelle: Graph

some coverage of Isabelle/Scala tools;
2012-04-28, by wenzelm
some coverage of Isabelle/jEdit;
2012-04-28, by wenzelm
some manual updates;
2012-04-28, by wenzelm
some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x;
2012-04-28, by wenzelm
add isar-ref documentation for transfer package
2012-04-28, by huffman
less confusion in NEWS
2012-04-28, by haftmann
rhs of abstract code equations are not subject to preprocessing: inline code abbrevs explicitly
2012-04-28, by haftmann
renamed Semi to Seq
2012-04-28, by nipkow
merged
2012-04-27, by wenzelm
prefer Context_Position.report_generic, which observes is_visible flag and thus reduces number of echos;
2012-04-27, by wenzelm
clarified signature;
2012-04-27, by wenzelm
avoid spurious warning in invisible context, notably Haftmann-Wenzel sandwich;
2012-04-27, by wenzelm
made Context_Position independent from Config;
2012-04-27, by wenzelm
use Nitpick as an oracle for finite problems
2012-04-27, by blanchet
add extensionality to first-order provers
2012-04-27, by blanchet
avoid duplicate helpers
2012-04-27, by blanchet
mention tools and packages earlier;
2012-04-27, by wenzelm
tuned;
2012-04-27, by wenzelm
tuned;
2012-04-27, by wenzelm
tuned;
2012-04-27, by wenzelm
tuned;
2012-04-27, by wenzelm
merged
2012-04-27, by wenzelm
allow transfer tactic to leave extra unsolved subgoals if transfer rules are missing
2012-04-27, by huffman
documentation for the Lifting package in Isar-ref
2012-04-27, by kuncar
added darwin targets;
2012-04-27, by wenzelm
chmod -x;
2012-04-27, by wenzelm
multi-platform build script and component settings;
2012-04-27, by wenzelm
print errors on stderr;
2012-04-27, by wenzelm
general exec_process -- nothing specific to Cygwin;
2012-04-27, by wenzelm
more direct exec with synchronous exit code;
2012-04-27, by wenzelm
some updates on classic README, reduce the impression that there is much to install manually;
2012-04-27, by wenzelm
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
2012-04-27, by blanchet
move LEO-II closer to the top, for testing
2012-04-27, by blanchet
get rid of old CASC setup and move the arithmetic part to a new theory
2012-04-27, by blanchet
smaller batches, to play safe
2012-04-27, by blanchet
move file to where it belongs
2012-04-27, by blanchet
implement transfer tactic with more scalable forward proof methods
2012-04-27, by huffman
tuning
2012-04-27, by blanchet
tweak LEO-II setup
2012-04-27, by blanchet
eta-expand unapplied equalities in THF rather than using a proxy
2012-04-27, by blanchet
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
cold-start HOME is user.home, in accordance with Cygwin-Terminal.bat;
2012-04-24, by wenzelm
chmod -x;
2012-04-24, by wenzelm
augment Isabelle home directory more systematically;
2012-04-24, by wenzelm
Cygwin setup via the quasi-mirror isabelle.in.tum.de, which serves a fixed (downgraded) version;
2012-04-24, by wenzelm
prevent change of directory, by pretending we are the "Command Here" utility;
2012-04-24, by wenzelm
typo
2012-04-24, by nipkow
the perennial doc problem of how to define lists a second time
2012-04-24, by nipkow
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
2012-04-24, by blanchet
updated doc
2012-04-24, by blanchet
add a timeout on the monotonicity check
2012-04-24, by blanchet
handle TPTP definitions as definitions in Nitpick rather than as axioms
2012-04-24, by blanchet
get rid of old parser, hopefully for good
2012-04-24, by blanchet
fix handling of atomizable conjectures without a top-level "Trueprop" (e.g. "x == (y::nat)")
2012-04-24, by blanchet
run Mirabelle in quick and dirty mode
2012-04-24, by blanchet
doc update
2012-04-24, by nipkow
scrollable text;
2012-04-23, by wenzelm
bundle Cygwin-Terminal.bat;
2012-04-23, by wenzelm
basic Cygwin-Terminal for main Isabelle directory;
2012-04-23, by wenzelm
moved to ~isatest/.bashrc to accomodate AFP;
2012-04-23, by wenzelm
merged
2012-04-23, by wenzelm