isabelle: Graph

more official Thm.eq_thm_strict, without demanding ML equality type;
2013-07-17, by wenzelm
tuned;
2013-07-17, by wenzelm
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
2013-07-17, by immler
merged
2013-07-16, by wenzelm
Cygwin with Latex according to Cygwin-Latex-Setup.bat (presently unused);
2013-07-16, by wenzelm
overwrite target;
2013-07-16, by wenzelm
fully-automated packaging (requires Mac OS X);
2013-07-16, by wenzelm
more robust application init;
2013-07-16, by wenzelm
more self-contained application, with side-entry for init;
2013-07-16, by wenzelm
dispose intermediate 7z archive;
2013-07-16, by wenzelm
prefer stand-alone javaw;
2013-07-16, by wenzelm
more robust executable path specifications;
2013-07-16, by wenzelm
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
2013-07-16, by wenzelm
build Windows application on the spot, using Unix tools;
2013-07-16, by wenzelm
recover Cygwin symlinks via Windows file-system operations;
2013-07-15, by wenzelm
produce 7z archive for windows and preserve symlinks separately;
2013-07-15, by wenzelm
Scala version of init.bat;
2013-07-15, by wenzelm
tuned line length;
2013-07-15, by wenzelm
prefer @{file} references that are actually checked;
2013-07-15, by wenzelm
deactivate/revoke mouse event more thoroughly, to avoid "Implicit change of text area buffer";
2013-07-15, by wenzelm
retain compile-time context visibility, which is particularly important for "apply tactic";
2013-07-15, by wenzelm
use transfer/lifting for proving countable set and multisets being BNFs
2013-07-16, by traytel
added exercise
2013-07-16, by nipkow
killed unused theorems
2013-07-15, by traytel
eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
2013-07-15, by traytel
tuned specifications and proofs;
2013-07-15, by wenzelm
tuned;
2013-07-15, by wenzelm
keep persistent prints only if actually finished;
2013-07-15, by wenzelm
more careful termination of removed execs, leaving running execs undisturbed;
2013-07-15, by wenzelm
recover static nnf_ss from 6c0de045d127 -- avoid odd runtime warnings due to duplication of not_not;
2013-07-14, by wenzelm
merged
2013-07-13, by wenzelm
avoid spurious warnings, notably of 'try0' about already declared simps etc.;
2013-07-13, by wenzelm
initial delay for automatically tried tools;
2013-07-13, by wenzelm
more rendering for information messages;
2013-07-13, by wenzelm
update_options with full update, e.g. required for re-assignment of Command.prints;
2013-07-13, by wenzelm
tuned;
2013-07-13, by wenzelm
determine print function parameters dynamically, e.g. depending on runtime options;
2013-07-13, by wenzelm
NEWS;
2013-07-13, by wenzelm
clarified some default options;
2013-07-13, by wenzelm
gutter icon for information messages;
2013-07-13, by wenzelm
more explicit Markup.information for messages produced by "auto" tools;
2013-07-13, by wenzelm
full merge of Command.State, which enables Command.prints to augment markup as well (assuming that these dynamic overlays are relatively few);
2013-07-13, by wenzelm
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
2013-07-13, by wenzelm
compile
2013-07-13, by wenzelm
system options for Isabelle/HOL proof tools;
2013-07-12, by wenzelm
removed unused Predicate_Compile component setup;
2013-07-12, by wenzelm
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
2013-07-13, by haftmann
tuned variable names
2013-07-13, by haftmann
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
2013-07-13, by traytel
some new lemmas towards getting rid of in_bd BNF property; tuned
2013-07-11, by traytel
tuned
2013-07-13, by smolkas
added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
2013-07-12, by smolkas
merged
2013-07-12, by wenzelm
more robust proof export / import due to Stefan Berghofer;
2013-07-12, by wenzelm
added blast, force
2013-07-12, by smolkas
removed |>! and #>!
2013-07-12, by smolkas
tuned
2013-07-12, by smolkas
cleaner preplay interface
2013-07-12, by smolkas
tuned;
2013-07-12, by wenzelm
tuned proofs;
2013-07-12, by wenzelm
updated keywords;
2013-07-12, by wenzelm
localized and modernized adhoc-overloading (patch by Christian Sternagel);
2013-07-12, by wenzelm
merged
2013-07-12, by wenzelm
tuned proof;
2013-07-12, by wenzelm
reraise interrupts outside command regular transactions -- relevant for memo_stable;
2013-07-12, by wenzelm
added "isabelle update_sub_sup" tool;
2013-07-12, by wenzelm
allow spaces in file names;
2013-07-12, by wenzelm
more robust identifier syntax: sub/superscript counts as modifier of LETDIG part instead of LETTER, both isub/isup and sub/sup are allowed;
2013-07-10, by wenzelm
added |>! and #>! for convenient printing of timing information
2013-07-12, by smolkas
preplay failures might be resolved later, so proceed as usual
2013-07-12, by smolkas
more reasonable preplay_interface semantics
2013-07-12, by smolkas
tuned
2013-07-12, by smolkas
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
2013-07-12, by smolkas
merged
2013-07-12, by wenzelm
clarified memo_exec: plain synchronized access without any special tricks;
2013-07-12, by wenzelm
tuned;
2013-07-12, by wenzelm
clarified execution: maintain running execs only, check "stable" separately via memo (again);
2013-07-12, by wenzelm
tuned signature;
2013-07-12, by wenzelm
clarified module name;
2013-07-12, by wenzelm
more explicit type Exec.context;
2013-07-11, by wenzelm
tuned signature;
2013-07-11, by wenzelm
strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
2013-07-11, by wenzelm
tuned -- cleanup before publishing assignment;
2013-07-11, by wenzelm
more abstract types;
2013-07-11, by wenzelm
tuned;
2013-07-11, by wenzelm
disallow concurrent execution attempt explicitly -- it should never happen due to management of singleton execution;
2013-07-11, by wenzelm
more precise fact declarations -- fewer warnings;
2013-07-11, by wenzelm
global management of command execution fragments;
2013-07-11, by wenzelm
fully synchronized guard of running execution;
2013-07-11, by wenzelm
merged
2013-07-11, by nipkow
added exercises
2013-07-11, by nipkow
optimize isar-proofs by trying different proof methods
2013-07-11, by smolkas
made SML/NJ happy
2013-07-11, by smolkas
tuned
2013-07-11, by smolkas
tuned;
2013-07-11, by wenzelm
re-assign prints of unchanged eval only -- avoid crash of new_exec;
2013-07-11, by wenzelm
tuned -- refrain from odd optimization;
2013-07-11, by wenzelm
tuned;
2013-07-11, by wenzelm
added "echo" command for demonstration purposes;
2013-07-10, by wenzelm
more abstract message channel;
2013-07-10, by wenzelm
explicit shutdown of message output thread;
2013-07-10, by wenzelm
tuned signature;
2013-07-10, by wenzelm
no need for raw stdin;
2013-07-10, by wenzelm
fall back on synchronous message output for single-threaded SML/NJ;
2013-07-10, by wenzelm
make SML/NJ happy;
2013-07-10, by wenzelm
retain main thread for protocol loop -- no access to raw ML toplevel;
2013-07-10, by wenzelm
removed historic dimacs2hol (see also read_dimacs_cnf_file in src/HOL/Tools/sat_solver.ML);
2013-07-10, by wenzelm
less intrusive token_range rendering, which is relevant for inner parse errors;
2013-07-10, by wenzelm
made SML/NJ happy
2013-07-10, by smolkas
merged
2013-07-10, by wenzelm
tuned start_execution: avoid sleep on worker thread;
2013-07-10, by wenzelm
print "persistent" flag allows to adjust tradeoff of ML run-time vs. JVM heap-space;
2013-07-10, by wenzelm
allow to remove print functions;
2013-07-10, by wenzelm
clarified Command.print: update old prints here;
2013-07-10, by wenzelm
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
2013-07-09, by wenzelm
tuned;
2013-07-09, by wenzelm
tuned proofs;
2013-07-09, by wenzelm
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
2013-07-09, by wenzelm
tuned message;
2013-07-09, by wenzelm
tuned signature -- NB: Command.read is actually part of Command.eval;
2013-07-09, by wenzelm