isabelle: Graph

tuned proofs;
2015-09-13, by wenzelm
renamed method "goals" to "goal_cases" to emphasize its meaning;
2015-09-13, by wenzelm
tuned proofs;
2015-09-13, by wenzelm
method "goals" ignores facts;
2015-09-13, by wenzelm
tuned;
2015-09-13, by wenzelm
unconceal symbols stemming from inductive_set specifications, which are regular part of user-space specification;
2015-09-10, by haftmann
fully detached test run, to avoid flashing window on Windows with Cygwin-Terminal;
2015-09-11, by wenzelm
single-instance application on Windows;
2015-09-11, by wenzelm
more robust init_components: test run of polyml executable on windows appears to disrupt stdin stream of cygwin;
2015-09-11, by wenzelm
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
2015-09-11, by wenzelm
clarified order;
2015-09-11, by wenzelm
more symbols;
2015-09-11, by wenzelm
Unicode is standard in Poly/ML repository version;
2015-09-10, by wenzelm
removed obsolete undocumented feature;
2015-09-10, by wenzelm
more standard local_theory operations;
2015-09-10, by wenzelm
HOL-Proofs is slow;
2015-09-10, by wenzelm
convenient access to application properties;
2015-09-10, by wenzelm
tuned -- avoid slightly odd @{cpat};
2015-09-10, by wenzelm
dropped redundant NEWS
2015-09-10, by haftmann
less ambitious options, to accomodate 4GB systems;
2015-09-10, by wenzelm
tuned
2015-09-10, by nipkow
clarified declaration flags, like 'declaration' command;
2015-09-09, by wenzelm
merged
2015-09-09, by wenzelm
simplified simproc programming interfaces;
2015-09-09, by wenzelm
eliminated \<Colon> from syntax of constraints;
2015-09-09, by wenzelm
eliminated \<Colon> -- from dead code!
2015-09-09, by wenzelm
merged
2015-09-09, by Andreas Lochbihler
reactivate examples with predicate compiler and quickcheck
2015-09-09, by Andreas Lochbihler
disable jedit_auto_resolve (again) -- too confusing;
2015-09-08, by wenzelm
proper Windows path, notably for ML basis;
2015-09-08, by wenzelm
more basic Windows path operations -- evade exception InvalidArc with Unicode;
2015-09-08, by wenzelm
updated to polyml-5.5.3-20150908, with support for x86_64-windows and Unicode file-names;
2015-09-08, by wenzelm
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
2015-09-08, by wenzelm
clarified Java runtime options for 32 vs. 64 bit;
2015-09-08, by wenzelm
clarified JEDIT_JAVA_OPTIONS: separate defaults for 32 vs. 64 bit;
2015-09-08, by wenzelm
clarified JEDIT_JAVA_SYSTEM_OPTIONS;
2015-09-08, by wenzelm
clarified ISABELLE_BUILD_JAVA_OPTIONS;
2015-09-08, by wenzelm
unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup
2015-09-06, by haftmann
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
2015-09-06, by haftmann
formally regenerated
2015-09-06, by haftmann
tuned notation, proofs, namespace
2015-09-06, by haftmann
obsolete: if case_prod is fully applied, it is printed as proper case expression;
2015-09-06, by haftmann
prefer "uncurry" as canonical name for case distinction on products in combinatorial view
2015-09-06, by haftmann
tuned
2015-09-06, by haftmann
obsolete: all (formally unchecked) examples given in the comments work out of the box as advertised
2015-09-06, by haftmann
dropped whitespace leftover from b57df8eecad6
2015-09-06, by haftmann
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
2015-09-06, by wenzelm
tuned proofs;
2015-09-06, by wenzelm
removed obsolete theory Legacy_Mrec;
2015-09-06, by wenzelm
NEWS;
2015-09-06, by wenzelm
merged
2015-09-04, by wenzelm
close derivation *before* splitting conjuncts, like Goal.prove_common (see also 757cad5a3fe9) -- potential improvement of performance;
2015-09-04, by wenzelm
modernized name space management -- more uniform qualification;
2015-09-04, by wenzelm
tuned -- do not open ML structures;
2015-09-04, by wenzelm
trim context for persistent storage;
2015-09-04, by wenzelm
trim context for persistent storage;
2015-09-04, by wenzelm
proper restore naming after close, which is important for packages that used nested targets internally, e.g. BNF datatype;
2015-09-04, by wenzelm
more general Typedef.bindings;
2015-09-03, by wenzelm
proper restore_naming after global qed, which is important to make Name_Space.transform_naming work properly, e.g. for "private typedef";
2015-09-03, by wenzelm
merged
2015-09-04, by Andreas Lochbihler
merged
2015-09-03, by Andreas Lochbihler
use quotient and lifting package;
2015-09-03, by Andreas Lochbihler
merged
2015-09-03, by paulson
new lemmas about vector_derivative, complex numbers, paths, etc.
2015-09-03, by paulson
trim context for persistent storage;
2015-09-03, by wenzelm
misc tuning and modernization;
2015-09-03, by wenzelm
use open/close_target rather than Local_Theory.restore to get polymorphic definitions;
2015-09-03, by traytel
clean name as in ML Completion.make;
2015-09-03, by wenzelm
use alphabetic order before history order;
2015-09-03, by wenzelm
eliminated pointless cterms;
2015-09-02, by wenzelm
trim context for persistent storage;
2015-09-02, by wenzelm
trim context for persistent storage;
2015-09-02, by wenzelm
trim context for persistent storage;
2015-09-02, by wenzelm
trim context for persistent storage;
2015-09-02, by wenzelm
trim context for persistent storage;
2015-09-02, by wenzelm
trim context for persistent storage;
2015-09-02, by wenzelm
trim context for persistent storage;
2015-09-02, by wenzelm
more thorough transfer;
2015-09-02, by wenzelm
clarified context;
2015-09-02, by wenzelm
more thorough transfer;
2015-09-02, by wenzelm
clarified context;
2015-09-02, by wenzelm
tuned message;
2015-09-02, by wenzelm
trim context for persistent storage;
2015-09-02, by wenzelm
trim context for persistent storage;
2015-09-02, by wenzelm
eliminated old 'defs';
2015-09-02, by wenzelm
expose locale definition to normal user-namespace (for completion, query etc.) -- in contrast to 149f80f27c84, ba9f52f56356, f7d9c5e5d2f9;
2015-09-02, by wenzelm
clarified vacuous binding;
2015-09-02, by wenzelm
trim context more thoroughly;
2015-09-02, by wenzelm
tuned;
2015-09-02, by wenzelm
updated sessions;
2015-09-02, by wenzelm
thread context for exceptions from forks, e.g. relevant when printing errors;
2015-09-01, by wenzelm
eliminated \<Colon>;
2015-09-01, by wenzelm
tuned -- avoid slightly odd @{cpat};
2015-09-01, by wenzelm
support x86_64-windows;
2015-08-31, by wenzelm
misc tuning and simplification;
2015-08-31, by wenzelm
proper option, not catch-all pattern;
2015-08-31, by wenzelm
support x86_64-windows;
2015-08-31, by wenzelm
prefer symbols;
2015-08-31, by wenzelm
prefer symbols;
2015-08-31, by wenzelm
proper qualified naming;
2015-08-31, by wenzelm
misc tuning and clarification;
2015-08-31, by wenzelm
misc tuning and modernization;
2015-08-31, by wenzelm
clarified context;
2015-08-31, by wenzelm
tuned signature;
2015-08-31, by wenzelm
clarified context;
2015-08-31, by wenzelm
tuned message;
2015-08-31, by wenzelm
trim context for persistent storage;
2015-08-31, by wenzelm
trim context for persistent storage;
2015-08-30, by wenzelm
trim context for persistent storage;
2015-08-30, by wenzelm
trim context for persistent storage;
2015-08-30, by wenzelm
trim context for persistent storage;
2015-08-30, by wenzelm
trim context for persistent storage;
2015-08-30, by wenzelm
store result of swapify, to avoid later access to implicit context;
2015-08-30, by wenzelm
trim context for persistent storage;
2015-08-30, by wenzelm
tuned;
2015-08-30, by wenzelm
clarified implicit context;
2015-08-30, by wenzelm
clarified exceptions;
2015-08-30, by wenzelm
clarified exceptions;
2015-08-30, by wenzelm
trim context for persistent storage;
2015-08-30, by wenzelm
trim context for persistent storage;
2015-08-30, by wenzelm
clarified exceptions;
2015-08-30, by wenzelm
tuned documentation -- merge is implicitly performed by the system;
2015-08-28, by wenzelm
clarified exceptions: avoid interference of formal context failure with regular rule application failure (which is routinely handled in user-space);
2015-08-28, by wenzelm
more abstract theory certificate, which is not necessarily the full theory;
2015-08-28, by wenzelm
eliminated obsolete environment variable
2015-08-28, by blanchet
tuned signature;
2015-08-28, by wenzelm
tuned;
2015-08-28, by wenzelm
tuned;
2015-08-28, by wenzelm
tuned signature;
2015-08-28, by wenzelm
tuned;
2015-08-28, by wenzelm
tuned signature;
2015-08-28, by wenzelm
clarified language context, e.g. relevant for symbols;
2015-08-28, by wenzelm
merged;
2015-08-28, by wenzelm
tuned;
2015-08-26, by wenzelm
generate proper error instead of exception if goal cannot be atomized
2015-08-27, by blanchet
standardized some occurences of ancient "split" alias
2015-08-27, by haftmann
more lemmas on sorting and multisets (due to Thomas Sewell)
2015-08-27, by haftmann
robust handling of Vampire 4 proofs
2015-08-27, by blanchet
reverted 6ac3172985d4 -- the old URL has been restored
2015-08-27, by blanchet
fixed typo in comment
2015-08-27, by blanchet
use fancy options of Java 8;
2015-08-26, by wenzelm
tuned signature;
2015-08-26, by wenzelm
clarified kill on Windows: just one executable;
2015-08-26, by wenzelm
avoid deprecated PluginOptions with its unbounded window size;
2015-08-25, by wenzelm
clarified undefined_blobs: already loaded theories are suppressed;
2015-08-25, by wenzelm
tuned spacing
2015-08-25, by nipkow
tuned exercise
2015-08-25, by nipkow
merged
2015-08-24, by wenzelm
reset focus after thread update (with new debug_states);
2015-08-24, by wenzelm
atomic Debugger.status;
2015-08-24, by wenzelm
tuned;
2015-08-24, by wenzelm
tuned;
2015-08-24, by wenzelm
more thorough GUI update;
2015-08-24, by wenzelm
maintain per-thread focus context;
2015-08-24, by wenzelm
typos
2015-08-24, by nipkow
nex exercise
2015-08-24, by nipkow
more explicit debugger caret rendering;
2015-08-24, by wenzelm
more explicit type Debugger.Context;
2015-08-23, by wenzelm
more precise tree re-selection;
2015-08-23, by wenzelm
proper GUI event;
2015-08-23, by wenzelm
update focus more thoroughly;
2015-08-23, by wenzelm
tuned;
2015-08-22, by wenzelm
merged
2015-08-21, by traytel
don't use types that come from the database---they are inconsistent with the ones occurring in the terms
2015-08-21, by traytel
tuned;
2015-08-21, by wenzelm
clarified linux application bundle;
2015-08-21, by wenzelm
more version information;
2015-08-21, by wenzelm
separate bundle for windows64;
2015-08-21, by wenzelm
tuned;
2015-08-21, by wenzelm
more scalable GUI;
2015-08-21, by wenzelm
eliminated WinRun4J artifact;
2015-08-21, by wenzelm
proper classpath for launcher;
2015-08-21, by wenzelm
updated to jdk-8u60, with support for x86_64-windows;
2015-08-21, by wenzelm
updated to recent launch4j 3.8;
2015-08-21, by wenzelm
clarified modules;
2015-08-20, by wenzelm
clarified modules, like ML version;
2015-08-20, by wenzelm
clarified modules, like ML version;
2015-08-20, by wenzelm
suppress small CPU time, notably on x86-windows, where bash does not account for the poly process;
2015-08-20, by wenzelm
obsolete;
2015-08-20, by wenzelm
tuned signature, according to ML version;
2015-08-20, by wenzelm
The Stone-Weierstrass theorem
2015-08-20, by paulson
tuned;
2015-08-20, by wenzelm
obsolete;
2015-08-20, by wenzelm
NEWS;
2015-08-20, by wenzelm
updated to polyml-5.5.3-20150820, with native x86-windows support;
2015-08-20, by wenzelm
precise BinIO, without newline conversion on Windows;
2015-08-20, by wenzelm
repaired proofs after 6a6f15d8fbc4;
2015-08-19, by wenzelm
merged
2015-08-19, by wenzelm
clarified x86-windows setup;
2015-08-19, by wenzelm
proper check for Windows executables;
2015-08-19, by wenzelm
Cygwin bash on Windows;
2015-08-19, by wenzelm
tuned;
2015-08-19, by wenzelm