isabelle: Graph

Explicitly build HOLCF and ZF images. They are not part of the release any more.
2011-02-08, by kleing
added termination lemmas
2011-02-08, by nipkow
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
2011-02-07, by bulwahn
discontinued support for Poly/ML 5.2, which was the last version without proper multithreading and TimeLimit implementation;
2011-02-08, by wenzelm
tuned headers;
2011-02-08, by wenzelm
updated to polyml-5.3.0, which is presently known as the most robust version;
2011-02-08, by wenzelm
explicit Multithreading.interrupted to ensure that interrupts stay within the boundaries of managed evaluation blocks;
2011-02-08, by wenzelm
always test/clear Multithreading.interrupted, indepently of thread attributes;
2011-02-08, by wenzelm
added Multithreading.interrupted (cf. java.lang.Thread.interrupted);
2011-02-08, by wenzelm
more robust TimeLimit: make double sure that watchdog has terminated and interrupts received during uninterruptible state are propagated (NB: Thread.testInterrupt requires InterruptSynch in Poly/ML 5.4.0 or earlier);
2011-02-07, by wenzelm
more tracing information via Par_List.map_name;
2011-02-05, by wenzelm
clarified bootstrapping of structure TimeLimit;
2011-02-05, by wenzelm
more scalable collections of tasks, notably for totality of known group members;
2011-02-04, by wenzelm
tuned signature;
2011-02-04, by wenzelm
merged
2011-02-04, by wenzelm
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
2011-02-04, by hoelzl
add auto support for AE_mp
2011-02-04, by hoelzl
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
2011-02-04, by hoelzl
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
2011-02-04, by wenzelm
Task_Queue.update_timing: more precise treatment of interruptibility;
2011-02-04, by wenzelm
Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
2011-02-04, by wenzelm
thm_proof: visible fulfill_body only, without joining nested thms -- retain proof irrelevance, which is important for parallel performance;
2011-02-03, by wenzelm
tuned comments;
2011-02-03, by wenzelm
clarified Proofterm.proofs_enabled;
2011-02-03, by wenzelm
explicit is better than implicit;
2011-02-03, by wenzelm
tuned odd conditional expression;
2011-02-02, by wenzelm
eliminated slightly odd abstract type Task_Queue.deps;
2011-02-02, by wenzelm
merged
2011-02-02, by wenzelm
Introduction of metis calls and other cosmetic modifications.
2011-02-02, by paulson
merged
2011-02-02, by boehmes
avoid ML structure aliases (especially single-letter abbreviations)
2011-02-02, by boehmes
making the bash script swipl_version closer to Isabelle's conventional bash scripts
2011-02-02, by bulwahn
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
2011-02-02, by hoelzl
merged
2011-02-02, by bulwahn
scala serializer adds parentheses around function literals
2011-02-02, by bulwahn
made SML/NJ happy
2011-02-02, by krauss
term style 'isub': ad-hoc subscripting of variables that end with digits (x1, x23, ...)
2011-02-01, by krauss
refined Task_Queue.dequeue_deps (more incremental);
2011-02-02, by wenzelm
maintain Task_Queue.group within Task_Queue.task;
2011-02-02, by wenzelm
tuned comment;
2011-02-02, by wenzelm
Future.join_results: discontinued post-hoc recording of dynamic dependencies;
2011-02-02, by wenzelm
more informative task timing: some dependency tracking;
2011-02-01, by wenzelm
refined task timing: joining vs. waiting;
2011-02-01, by wenzelm
simplified trace;
2011-02-01, by wenzelm
more specific Goal.fork_name;
2011-01-31, by wenzelm
name "passive" tasks (practically lazy values);
2011-01-31, by wenzelm
tuned trivial cases;
2011-01-31, by wenzelm
tuned signature;
2011-01-31, by wenzelm
support named tasks, for improved tracing;
2011-01-31, by wenzelm
more direct Future.bulk, which potentially reduces overhead for Par_List;
2011-01-31, by wenzelm
tuned isatest settings;
2011-01-31, by wenzelm
added basic task timing;
2011-01-31, by wenzelm
some notes on Cygwin;
2011-01-31, by wenzelm
more platform hints;
2011-01-31, by wenzelm
merged
2011-01-31, by wenzelm
tuned;
2011-01-31, by wenzelm
back to post-release mode;
2011-01-31, by wenzelm
removed obsolete test tags;
2011-01-30, by wenzelm
removed Florian's email from isatest (bounces)
2011-01-28, by kleing
merged
2011-01-25, by hoelzl
use pre-image measure, instead of image
2011-01-24, by hoelzl
use AE_mp in AE_conjI proof
2011-01-21, by hoelzl
tuned proof
2011-01-19, by hoelzl
merged
2011-01-21, by haftmann
moved theorem
2011-01-21, by haftmann
restructured theory;
2011-01-21, by haftmann
merged
2011-01-19, by hoelzl
Gauge measure removed
2011-01-18, by hoelzl
merged
2011-01-18, by haftmann
report mutabelle log in mira configuration
2011-01-18, by haftmann
back to post-release mode;
2011-01-17, by wenzelm
delete .elc files unconditionally -- they cause too many incompatibilities;
2011-01-30, by wenzelm
Added tag Isabelle2011 for changeset 6d736d983d5c
2011-01-30, by wenzelm
clarified example settings for Proof General; Isabelle2011
2011-01-30, by wenzelm
adhoc patches relative to ProofGeneral-4.1pre101216, which has setprefs working;
2011-01-28, by wenzelm
more precise stats;
2011-01-28, by wenzelm
some adhoc patches for ProofGeneral-4.1pre110112;
2011-01-28, by wenzelm
enforce STIXGeneral, which is preferred by PG 4.1;
2011-01-28, by wenzelm
default UTF-8 locale, to work with funny base directory (e.g. Chinese);
2011-01-28, by wenzelm
enforce fonts;
2011-01-28, by wenzelm
added option -f FONT;
2011-01-27, by wenzelm
Proof General 4.x interface wrapper;
2011-01-27, by wenzelm
old Proof General patches;
2011-01-27, by wenzelm
Added tag isa2011-test3 for changeset 55a45051b220
2011-01-27, by wenzelm
Tuned definition of sdiv.
2011-01-27, by berghofe
CRITICAL markup for critical poking with unsynchronized references;
2011-01-27, by wenzelm
Replaced smod by standard mod operator to reflect actual behaviour
2011-01-26, by berghofe
cancel document execution before editing, to improve reactivity on systems with few cores;
2011-01-27, by wenzelm
tuned isatest settings (for Poly/ML SVN 1278);
2011-01-25, by wenzelm
merged
2011-01-25, by wenzelm
do not restore old files on startup, which is potentially slow due to automatic rechecking;
2011-01-25, by wenzelm
singleton (sequential) execution, to avoid race conditions in theory loader state (e.g. when multiple independent theories import the same theory);
2011-01-25, by wenzelm
workaround for odd x86_64 problem in Poly/ML 5.4.0 (actually SVN 1151?), which causes unexpected nontermination of Isabelle/Scala document editing;
2011-01-25, by wenzelm
improved README -- Isabelle symbols and fonts;
2011-01-24, by wenzelm
delete compiled .elc files to improve portability on Linux, notably for GNU Emacs 23.1.x instead of 23.2.x;
2011-01-24, by wenzelm
do not overwrite proof-shell-quit-timeout by default (final PG 4.1 supposedly gets it right);
2011-01-23, by wenzelm
Added tag isa2011-test2 for changeset 237328506a42
2011-01-23, by wenzelm
Documented unused_thms
2011-01-23, by berghofe
JVM/Windows: more robust treatment of unicode in file names;
2011-01-21, by wenzelm
java/scala: default to UTF-8;
2011-01-21, by wenzelm
updated Named_Target.init;
2011-01-21, by wenzelm
made SML/NJ happy;
2011-01-21, by wenzelm
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
2011-01-20, by wenzelm
fixing list_to_set_comprehension simproc
2011-01-19, by bulwahn
more release checks;
2011-01-19, by wenzelm
potentially more robust utf8 handling (cf. 3e4bb6e7c3ca);
2011-01-19, by wenzelm
clasrified classpath: add in front in accordance to librarypath (cf. b7cd80330a16), for slightly more robustness;
2011-01-19, by wenzelm
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
2011-01-19, by wenzelm
merged
2011-01-19, by wenzelm
tuned;
2011-01-19, by wenzelm
Cygwin: back to ProofGeneral-3.7.1.1 with XEmacs, since PG 4.x with GNU Emacs 23 is painfully slow;
2011-01-19, by wenzelm
isabelle jedit as alternative;
2011-01-18, by wenzelm
Apple's way of locating java;
2011-01-18, by wenzelm
more notes on final release stage;
2011-01-18, by wenzelm
makedist: refer to isabelle-release;
2011-01-17, by wenzelm
Added tag isa2011-test1 for changeset 7d035da21e9c
2011-01-17, by wenzelm
tuned;
2011-01-17, by wenzelm
some announcement;
2011-01-17, by wenzelm
tuned;
2011-01-17, by wenzelm
merged
2011-01-17, by wenzelm
made Z3 the default SMT solver again
2011-01-17, by boehmes
some notes on final release stage;
2011-01-17, by wenzelm
isatest: run at-poly on macbroy28 for slightly more robust isatest-doc;
2011-01-17, by wenzelm
keep Proof General 4.0 and 3.7.1.1 for now;
2011-01-17, by wenzelm
tuned;
2011-01-16, by wenzelm
misc updates for release;
2011-01-16, by wenzelm
tuned;
2011-01-16, by wenzelm
misc tuning for release;
2011-01-16, by wenzelm
merged
2011-01-16, by wenzelm
Tuned show_status
2011-01-16, by berghofe
proper type variables with sorts;
2011-01-16, by wenzelm
non-executable sources;
2011-01-16, by wenzelm
tuned headers;
2011-01-16, by wenzelm
tuned;
2011-01-16, by wenzelm
type_synonym;
2011-01-16, by wenzelm
more standard command descriptions;
2011-01-16, by wenzelm
added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
2011-01-16, by wenzelm
Replaced ad-hoc advance function by Position.advance
2011-01-15, by berghofe
merged
2011-01-15, by wenzelm
experimental variant of interpretation with simultaneous definitions, plus example
2011-01-15, by haftmann
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
2011-01-15, by wenzelm
link HOL-Proofs/index.html, which is not reachable from regular HOL/index.html;
2011-01-15, by wenzelm
type_synonym;
2011-01-15, by wenzelm
recovered printing of record updates over compound terms, e.g. "(|x = a|)(|x := b|)", which was apparently broken in 45a2ffc5911e;
2011-01-15, by wenzelm
export Record.get_hierarchy -- external tools typically need this information;
2011-01-15, by wenzelm
tuned;
2011-01-15, by wenzelm
removed unreferenced identifiers;
2011-01-15, by wenzelm
global "prems" is legacy feature;
2011-01-15, by wenzelm
misc updates for release;
2011-01-15, by wenzelm
merged;
2011-01-15, by wenzelm
misc tuning for release;
2011-01-15, by wenzelm
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
2011-01-15, by boehmes
Also added SPARK to test and clean targets.
2011-01-15, by berghofe
merged
2011-01-15, by berghofe
Added entry for HOL-SPARK
2011-01-15, by berghofe
Added HOL-SPARK and removed old_primrec.ML
2011-01-15, by berghofe
unused_thms no longer compares propositions, since this is no longer needed
2011-01-15, by berghofe
Include HOL-SPARK keywords
2011-01-15, by berghofe
Include HOL-SPARK
2011-01-15, by berghofe
Finally removed old primrec package, since Primrec.add_primrec_global
2011-01-15, by berghofe
Added new SPARK verification environment.
2011-01-15, by berghofe
remove presently unused Isabelle application for official releases;
2011-01-15, by wenzelm
hardwired default for proof-shell-quit-timeout (PG 4.1 provides rather low value);
2011-01-15, by wenzelm
treat HOLCF as HOL library session, not as "logic";
2011-01-15, by wenzelm
increased startup-timeout to accommodate slow systems (especially Windows/Cygwin);
2011-01-15, by wenzelm
bundle main HOL image only, to save about 300 MB disk space;
2011-01-14, by wenzelm
updated for release;
2011-01-14, by wenzelm
adjusted mira configuration
2011-01-14, by haftmann
merged
2011-01-14, by wenzelm
global "prems" is legacy feature;
2011-01-14, by wenzelm
tuned markup;
2011-01-14, by wenzelm
eliminated global prems;
2011-01-14, by wenzelm
more precise import;
2011-01-14, by wenzelm
Thy_Load.begin_theory: maintain source specification of imports;
2011-01-14, by wenzelm
merged
2011-01-14, by hoelzl
integral on lebesgue measure is extension of integral on borel measure
2011-01-14, by hoelzl
tuned formalization of subalgebra
2011-01-14, by hoelzl
introduced integral syntax
2011-01-14, by hoelzl
tuned theorem order
2011-01-14, by hoelzl
configuration file for mira
2011-01-14, by haftmann
eliminated global prems;
2011-01-13, by wenzelm
more precise pretty printing -- to accomodate Scala message layout;
2011-01-13, by wenzelm
less verbosity -- avoid slightly odd tracing information on warning channel;
2011-01-13, by wenzelm
updated Isabelle/jEdit limitations and workarounds;
2011-01-13, by wenzelm
full theory path enables loading parents via master directory and keeps files strictly separate;
2011-01-13, by wenzelm
Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
2011-01-13, by wenzelm
clarified split_thy_path;
2011-01-13, by wenzelm
less verbosity;
2011-01-13, by wenzelm
proper 'domain' class instance for 'a defl, with deflation combinator
2011-01-12, by huffman
documented Option.bind
2011-01-12, by krauss
CONTRIBUTORS
2011-01-12, by krauss
updated keywords;
2011-01-12, by wenzelm
eliminated global prems;
2011-01-12, by wenzelm
eliminated global prems;
2011-01-12, by wenzelm
updated to ProofGeneral-4.x;
2011-01-12, by wenzelm
eliminated global prems;
2011-01-12, by wenzelm
tuned proof;
2011-01-12, by wenzelm
eliminated global prems;
2011-01-12, by wenzelm
compile;
2011-01-12, by wenzelm
more FIXMEs concerning bad catch-all exception handlers;
2011-01-12, by wenzelm
eliminated obsolete print_sign_exn_unit;
2011-01-12, by wenzelm
reraise interrupts as usual;
2011-01-12, by wenzelm
avoid catch-all exception handler, presumably TERM was meant here;
2011-01-12, by wenzelm
disabled experimental treatment of replacement text for now, which leads to odd spacing and strange effects on non-poppler viewers;
2011-01-12, by wenzelm
observe line length limit;
2011-01-12, by wenzelm
smart_string_of_real: print integer values without fractional part;
2011-01-12, by wenzelm
tuned (cf. 2fe62d602681);
2011-01-11, by wenzelm
added dist/jedit symlink for convenience;
2011-01-11, by wenzelm
record versions of both jEdit and Isabelle;
2011-01-11, by wenzelm
updated to Isabelle2011;
2011-01-11, by wenzelm
isabelle version -i;
2011-01-11, by wenzelm
NEWS
2011-01-11, by haftmann
NEWS
2011-01-11, by bulwahn
eliminated duplication
2011-01-11, by krauss
merged
2011-01-11, by wenzelm
tuned text
2011-01-11, by haftmann
"enriched_type" replaces less specific "type_lifting"
2011-01-11, by haftmann
clarified notion Position.is_reported;
2011-01-11, by wenzelm
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
2011-01-10, by wenzelm
refined ML_Lex.flatten: ensure proper separation of tokens;
2011-01-10, by wenzelm
ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
2011-01-10, by wenzelm
use just one data slot to VC-related information
2011-01-10, by boehmes
be more precise: also merge option values
2011-01-10, by boehmes
only print warning in a visible context (previously, the warning was printed more than once)
2011-01-10, by boehmes
dropped superfluous error message
2011-01-10, by boehmes
removed obsolete make target (now in doc-src, cf. 28b487cd9e15)
2011-01-10, by krauss
updated for polyml-5.4.0;
2011-01-10, by wenzelm
made SML/NJ happy;
2011-01-10, by wenzelm
added merge_options convenience;
2011-01-10, by wenzelm
tuned string_of_int to avoid allocation for small integers;
2011-01-10, by wenzelm
eliminated Int.toString;
2011-01-10, by wenzelm
eliminated obsolete LargeInt -- Int is unbounded;
2011-01-10, by wenzelm
standardized split_last/last_elem towards List.last;
2011-01-10, by wenzelm
removing dead code; tuned
2011-01-10, by bulwahn
made SML/NJ happy
2011-01-10, by bulwahn
reverted 08240feb69c7 -- breaks positions of reports;
2011-01-09, by wenzelm
ML_trace: observe context visibility flag (import for Latex mode, for example);
2011-01-09, by wenzelm
more direct treatment of Position.end_offset;
2011-01-09, by wenzelm
discontinued unused end_line, end_column;
2011-01-09, by wenzelm
more scalable HTML.output_width;
2011-01-09, by wenzelm