isabelle: Graph

misc tuning and modernization;
2016-11-01, by wenzelm
always expand equalities in the transfer relation in transfer_prover (cf. 0a7c97c76f46)
2016-10-31, by kuncar
moved contribution to right release
2016-10-31, by blanchet
more explicit pull;
2016-10-31, by wenzelm
types to sets: initial commit
2016-10-30, by kuncar
avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar
2016-10-29, by blanchet
adapted Nunchaku integration to keyword renaming
2016-10-29, by blanchet
tuned;
2016-10-28, by wenzelm
merged
2016-10-28, by wenzelm
Added tag Isabelle2016-1-RC1 for changeset 9ee2480d10b7
2016-10-28, by wenzelm
a more general relator domain rule for the function type
2016-10-28, by kuncar
Haskabelle is presently unmaintained;
2016-10-28, by wenzelm
tuned;
2016-10-28, by wenzelm
merged
2016-10-27, by wenzelm
more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
2016-10-27, by wenzelm
avoid multiple PIDE markup due to (potentially infinite) backtracking;
2016-10-27, by wenzelm
more permissive remote_build_history: failure happens routinely and should not lead error, without saving logs;
2016-10-27, by wenzelm
more lemmas
2016-10-27, by fleury
updated CVC4 component
2016-10-27, by blanchet
tuning
2016-10-27, by blanchet
more uniform treatment of codatatype vs. datatype map and rel theorem generation (towards nonuniform codatatypes)
2016-10-27, by blanchet
added lemma
2016-10-27, by nipkow
tuning
2016-10-26, by blanchet
preprocess typedefs and quotients correctly
2016-10-26, by blanchet
adapted Nunchaku's input syntax to new design decisions
2016-10-26, by blanchet
more informative error (see 6e9c22c494c5);
2016-10-26, by wenzelm
tuned signature -- more friendly for experimentation;
2016-10-26, by wenzelm
clarified hg push return code: 1 means "nothing to push";
2016-10-26, by wenzelm
proper Nunchaku setup to use CVC4 and Kodkod
2016-10-26, by blanchet
more specific hardware information: relevant for ultimate Mac OS X version;
2016-10-26, by wenzelm
just one task to identify Isabelle + AFP repository snapshots and build release;
2016-10-26, by wenzelm
tuned;
2016-10-26, by wenzelm
Deleted spurious markup
2016-10-26, by paulson
latest Mac OS X versions *are* still supported, but presently without formal reference systems;
2016-10-26, by wenzelm
pagecolor no longer exists;
2016-10-25, by wenzelm
merged
2016-10-25, by wenzelm
use other remote_mac: macbroy30 is down;
2016-10-25, by wenzelm
more robust printing of names in the context of outer syntax;
2016-10-25, by wenzelm
more informative error (stderr);
2016-10-25, by wenzelm
more new material
2016-10-25, by paulson
Merge
2016-10-25, by paulson
more new material
2016-10-25, by paulson
tuned and updated for release;
2016-10-25, by wenzelm
updated for release;
2016-10-25, by wenzelm
tuned;
2016-10-25, by wenzelm
misc tuning for release;
2016-10-25, by wenzelm
added Nunchaku integration
2016-10-24, by blanchet
merged
2016-10-24, by wenzelm
version provided by web server;
2016-10-24, by wenzelm
proper default Windows ACLs, e.g. relevant when the bundle is placed into the root directory of a volume;
2016-10-24, by wenzelm
unused;
2016-10-24, by wenzelm
tuned documentation
2016-10-24, by blanchet
document limitations
2016-10-24, by blanchet
more accurate error message
2016-10-24, by blanchet
robustness
2016-10-24, by blanchet
document transfer_prover_eq and friend_of_corec_simps
2016-10-24, by Andreas Lochbihler
additional user-specified simp (naturality) rules used in friend_of_corec
2016-10-24, by traytel
apply transfer_prover after folding relator_eq
2016-10-24, by traytel
merged
2016-10-24, by wenzelm
more thorough cleanup of lib/classes -- it may contain broken Pure.jar or copies of Scala libraries (in historic versions);
2016-10-24, by wenzelm
remove old target: it is on the classpath and may break scalac;
2016-10-24, by wenzelm
updated to cygwin-20161024: cygwin.exe from current http://isabelle.in.tum.de/cygwin_2016-1
2016-10-24, by wenzelm
retain Admin component for isabelle tool invocation;
2016-10-24, by wenzelm
tuned;
2016-10-24, by wenzelm
more robust;
2016-10-24, by wenzelm
discontinued unused / untested distinction of separate PIDE modules;
2016-10-24, by wenzelm
proper Admin tool;
2016-10-24, by wenzelm
tuned message;
2016-10-24, by wenzelm
updated for release;
2016-10-24, by wenzelm
updated to jedit_build-20161024: Code2HTML 0.7, Navigator 2.7;
2016-10-24, by wenzelm
Merge
2016-10-24, by paulson
"subgoal" examples
2016-10-24, by paulson
Updated NEWS/CONTRIBUTORS w.r.t. Old_Number_Theory
2016-10-24, by eberlm
more readable output: whitespace is insignificant in HTML;
2016-10-23, by wenzelm
misc tuning and clarification;
2016-10-23, by wenzelm
modernized;
2016-10-23, by wenzelm
more operations;
2016-10-23, by wenzelm
more operations (see also properties.ML);
2016-10-23, by wenzelm
tuned signature: avoid conflict with "paragraph" as section heading;
2016-10-23, by wenzelm
tuned;
2016-10-23, by wenzelm
support for XML as HTML;
2016-10-23, by wenzelm
tuned;
2016-10-23, by wenzelm
more explicit rev (tip);
2016-10-23, by wenzelm
just one output file;
2016-10-23, by wenzelm
more tasks;
2016-10-22, by wenzelm
remote_builds has PAR-SEQ semantics of old isatest-makedist;
2016-10-22, by wenzelm
expose results on failure (via mail);
2016-10-22, by wenzelm
clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
2016-10-22, by wenzelm
support for URL notation;
2016-10-22, by wenzelm
process results immediately;
2016-10-22, by wenzelm
permissive rename operation (amending b265dd04d57d);
2016-10-22, by wenzelm
pro-forma update to cygwin_2016-1 (web service still missing);
2016-10-22, by wenzelm
updated to current Cygwin, after 2.6.0-1 from 31-Aug-2016;
2016-10-22, by wenzelm
regular user tool;
2016-10-22, by wenzelm
avoid deprecated Scala;
2016-10-22, by wenzelm
minor updates after fresh installation of virtual Windows 2012: retain old versions of mingw for this brittle build process;
2016-10-21, by wenzelm
misc tuning and updates;
2016-10-21, by wenzelm
clarified default args;
2016-10-21, by wenzelm
speculative support for latest Mac OS X versions -- no reference systems yet;
2016-10-21, by wenzelm
merged
2016-10-21, by wenzelm
more ambitious default;
2016-10-21, by wenzelm
updated to new structure Foreign;
2016-10-21, by wenzelm
HOL-Probability: Essential Supremum as Limsup over ae_filter
2016-10-21, by hoelzl
less ambitious test;
2016-10-21, by wenzelm
proper type for Poly/ML development version;
2016-10-21, by wenzelm
more operations;
2016-10-21, by wenzelm
more on sgn in linear ordered fields
2016-10-20, by haftmann
merged
2016-10-20, by wenzelm
test for Windows/Cygwin;
2016-10-20, by wenzelm
extra trim_line for the sake of Windows;
2016-10-20, by wenzelm
prevent sporadic disconnection;
2016-10-20, by wenzelm
check Windows file names, e.g. relavant for native Mercurial, but also for Isabelle/Scala;
2016-10-20, by wenzelm
tuned
2016-10-20, by nipkow
NEWS
2016-10-18, by nipkow
HOL-Probability: generalize theorems about cumulative distribution function
2016-10-20, by hoelzl
HOL-Probability: move stopping time from AFP/Markov_Models
2016-10-20, by hoelzl
HOL-Probability: generalize type of essential supremum
2016-10-20, by hoelzl
Repaired LaTeX in HOL-Data_Structures
2016-10-20, by eberlm
More on Fibonacci numbers
2016-10-20, by eberlm
build HTML library in Isabelle/Scala;
2016-10-20, by wenzelm
proper echo;
2016-10-20, by wenzelm
more robust bootstrap, e.g. when experimenting with Poly/ML repository changes;
2016-10-20, by wenzelm
updated to jdk-8u112;
2016-10-19, by wenzelm
basic SSH server configuration;
2016-10-19, by wenzelm
proper isabelle tool in Scala;
2016-10-19, by wenzelm
tuned;
2016-10-19, by wenzelm
merged
2016-10-19, by wenzelm
added system option "profiling";
2016-10-19, by wenzelm
replaced inefficient valid_accesses by is_valid_access, based on stored input accesses: e.g. relevant for Proof_Context.update_thms;
2016-10-18, by wenzelm
tuned signature, in accordance to Isabelle_System;
2016-10-18, by wenzelm
tuned;
2016-10-18, by wenzelm
clarified modules;
2016-10-18, by wenzelm
another attempt to squeeze a list into a property list entry;
2016-10-18, by wenzelm
report actual build_args;
2016-10-18, by wenzelm
more flexible multicore configuration;
2016-10-18, by wenzelm
clarified multiple props: result needs to fit on a single line within the log file;
2016-10-18, by wenzelm
clarified properties;
2016-10-18, by wenzelm
tuned;
2016-10-18, by wenzelm
support for free-form build tags;
2016-10-18, by wenzelm
explicit identification of builds and correlated build groups;
2016-10-18, by wenzelm
avoid spamming log file;
2016-10-18, by wenzelm
shared_home is default for classic isatest home setup;
2016-10-18, by wenzelm
add missing file Essential_Supremum.thy
2016-10-18, by hoelzl
Merge
2016-10-18, by paulson
Inserted necessary dependency
2016-10-18, by paulson
suitable logical type class for abs, sgn
2016-10-18, by haftmann
HOL-Analysis: move Function Topology from AFP/Ergodict_Theory; HOL-Probability: move Essential Supremum from AFP/Lp
2016-10-18, by hoelzl
Merge
2016-10-18, by paulson
more from moretop.ml
2016-10-18, by paulson
Jenkins: build in system mode again
2016-10-18, by Lars Hupel
Jenkins: configurable clean build
2016-10-18, by Lars Hupel
HOL-Analysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
2016-10-18, by hoelzl
HOL-Probability: move conditional expectation from AFP/Ergodic_Theory
2016-10-13, by hoelzl
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
2016-10-17, by eberlm
restored document structure after theory refactoring
2016-10-18, by haftmann
NEWS;
2016-10-17, by wenzelm
merged
2016-10-17, by wenzelm
merged
2016-10-17, by wenzelm
improved platform coverage: macbroy30, macbroy31;
2016-10-17, by wenzelm
eliminated unused argument;
2016-10-17, by wenzelm
accomodate Poly/ML repository version, which treats singleton strings as boxed;
2016-10-17, by wenzelm
re-use "threads" for --gcthreads;
2016-10-17, by wenzelm
merged
2016-10-17, by nipkow
setprod -> prod
2016-10-17, by nipkow
merged
2016-10-17, by wimmers
Modified transfer principle in HOL/NSA to cause less ho-unficiation
2016-10-17, by Simon Wimmer
merged
2016-10-17, by nipkow
updated to setsum -> sum
2016-10-17, by nipkow
setsum -> sum
2016-10-17, by nipkow
uniform Isabelle settings -- avoid picking up different JAVA_HOME;
2016-10-17, by wenzelm
isabelle build -N;
2016-10-16, by wenzelm
support for Non-Uniform Memory Access of separate CPU nodes;
2016-10-16, by wenzelm
proper result;
2016-10-16, by wenzelm
merged
2016-10-16, by wenzelm
merged
2016-10-16, by wenzelm
more thorough cleanup;
2016-10-16, by wenzelm
tuned;
2016-10-16, by wenzelm
removed useless operation -- would require bash_process wrapper;
2016-10-16, by wenzelm
tuned signature;
2016-10-16, by wenzelm
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
2016-10-16, by wenzelm
more robust;
2016-10-16, by wenzelm
sftp.mkdirs according to 2a5dbad75355;
2016-10-16, by wenzelm
more compression for big log files;
2016-10-16, by wenzelm
clarified setup_repository: more uniform pull vs. clone, without update;
2016-10-16, by wenzelm
proper setup of fresh repository;
2016-10-16, by wenzelm
clarified prover-specific rules
2016-10-16, by haftmann
dropped potentially explosive rule for groebner simpset, with no observable effect on examples
2016-10-16, by haftmann
simplified fact references
2016-10-16, by haftmann
avoid effectively subsumed rules;
2016-10-16, by haftmann
eliminated irregular aliasses
2016-10-16, by haftmann
avoid references to lemmas designed for prover tools
2016-10-16, by haftmann
clarified theorem names
2016-10-16, by haftmann
eliminated irregular aliasses
2016-10-16, by haftmann
more standardized theorem names for facts involving the div and mod identity
2016-10-16, by haftmann
transfer rules for divides relation on integer and natural
2016-10-16, by haftmann
more standardized names
2016-10-16, by haftmann
added lemma
2016-10-16, by haftmann
de-orphanized declaration
2016-10-16, by haftmann
tuned;
2016-10-15, by wenzelm
discontinued somewhat pointless cronjob.options -- compile-time constants are sufficient;
2016-10-15, by wenzelm
timeout as in former isatest-makeall;
2016-10-15, by wenzelm
more robust quasi-unique name;
2016-10-15, by wenzelm
clarified signature: more static types;
2016-10-15, by wenzelm
clarified hg.id operation, with explicit tip as default;
2016-10-15, by wenzelm
added remote_build_history tasks: parallel on several remote hosts;
2016-10-15, by wenzelm
added setup_repository;
2016-10-15, by wenzelm
more operations;
2016-10-15, by wenzelm
expand relatively to given environment, notably remote HOME;
2016-10-15, by wenzelm
tuned;
2016-10-15, by wenzelm
tuned signature;
2016-10-15, by wenzelm
tuned;
2016-10-15, by wenzelm
clarified treatment of non-text bytes;
2016-10-15, by wenzelm
remove invocation of build_history: results are reported via stdout;
2016-10-15, by wenzelm
clarified signature;
2016-10-15, by wenzelm
identify release;
2016-10-15, by wenzelm
prefer Isabelle standard Path;
2016-10-15, by wenzelm
clarified logs;
2016-10-15, by wenzelm
publish directly on webspace;
2016-10-15, by wenzelm
Jenkins: don't build in system mode
2016-10-15, by Lars Hupel
merged
2016-10-14, by wenzelm
cronjob: build release from repository snapshot;
2016-10-14, by wenzelm
more operations;
2016-10-14, by wenzelm
clarified file operations;
2016-10-14, by wenzelm
proper link;
2016-10-14, by wenzelm
explicit website directory;
2016-10-14, by wenzelm
proper path;
2016-10-14, by wenzelm
tuned messages;
2016-10-14, by wenzelm
clarified platform families vs. bundles;
2016-10-14, by wenzelm
more general operations;
2016-10-14, by wenzelm
website index for existing bundles;
2016-10-14, by wenzelm
tuned messages;
2016-10-14, by wenzelm
added option -p for platform families;
2016-10-14, by wenzelm
more formal Release_Info;
2016-10-14, by wenzelm
replaced shell script by Isabelle/Scala;
2016-10-13, by wenzelm
tuned;
2016-10-13, by wenzelm
tuned whitespace;
2016-10-13, by wenzelm
clarified;
2016-10-13, by wenzelm
tuned;
2016-10-13, by wenzelm
tuned message;
2016-10-13, by wenzelm
more robust wrt. old versions that use clear-text properties (e.g. Timing in build_history_base);
2016-10-13, by wenzelm
tuned;
2016-10-13, by wenzelm
integrity test of build_history vs. build_history_base;
2016-10-13, by wenzelm
clarified log_subdir vs. log_filename;
2016-10-13, by wenzelm
tuned;
2016-10-13, by wenzelm
tuned;
2016-10-13, by wenzelm
provide USER_HOME, such that symbolic Path.explode("~") can be used remotely;
2016-10-13, by wenzelm
tuned signature;
2016-10-13, by wenzelm
clarified modules;
2016-10-13, by wenzelm
allow to exclude named tasks;
2016-10-13, by wenzelm
support for separate sub-system options, independent of main Isabelle options;
2016-10-13, by wenzelm
tuned;
2016-10-13, by wenzelm
tuned;
2016-10-13, by wenzelm
more cleanup;
2016-10-13, by wenzelm
separate ISABELLE_HOME_USER (with its etc/settings);
2016-10-13, by wenzelm
renamed lemma to a more consistent name
2016-10-13, by Lars Hupel
tuned
2016-10-13, by Lars Hupel
remove accidentally oops'ed (and wrong) lemma
2016-10-13, by Lars Hupel
transfer lifting rule for numeral
2016-10-12, by haftmann
more standard naming convention
2016-10-12, by haftmann
tuned;
2016-10-12, by wenzelm
special case for local contrib, e.g. lxbroy10;
2016-10-12, by wenzelm
merged
2016-10-12, by wenzelm
tuned signature;
2016-10-12, by wenzelm
tuned;
2016-10-12, by wenzelm
clarified task logging via log service;
2016-10-12, by wenzelm
more explicit management of tasks;
2016-10-12, by wenzelm
tuned;
2016-10-12, by wenzelm
added clone_repository;
2016-10-12, by wenzelm
support remote repositories via ssh command execution;
2016-10-12, by wenzelm
tuned signature;
2016-10-12, by wenzelm
modernized;
2016-10-12, by wenzelm
separate type class for arbitrary quotient and remainder partitions
2016-10-12, by haftmann
stripped dependency on pragmatic type class semiring_div
2016-10-11, by haftmann
simplified: no internal state for Mercurial;
2016-10-12, by wenzelm
explicit indication of Admin tools;
2016-10-12, by wenzelm
clarified files;
2016-10-12, by wenzelm
explicit timezone for the sake of lxbroy10;
2016-10-12, by wenzelm
proper redirection;
2016-10-11, by wenzelm
tuned output;
2016-10-11, by wenzelm
tuned message -- more parsable;
2016-10-11, by wenzelm
tuned signature;
2016-10-11, by wenzelm
identify managed repository clones;
2016-10-11, by wenzelm
some timing and logging, similar to old isatest.log;
2016-10-11, by wenzelm
enforce short name, notably on Mac OS X;
2016-10-11, by wenzelm
tuned -- Date.Format.default used by toString;
2016-10-11, by wenzelm
clarified modules;
2016-10-11, by wenzelm
force fresh build;
2016-10-11, by wenzelm
basic setup for Isabelle cronjob;
2016-10-11, by wenzelm
tuned;
2016-10-11, by wenzelm
merged
2016-10-11, by wenzelm
build on macbroy2 for performance, but use macbroy30 for its more robust hdiutil;
2016-10-11, by wenzelm
makedist_bundle works on Linux as well: build dmg on remote Mac;
2016-10-11, by wenzelm
added isabelle remote_dmg tool;
2016-10-11, by wenzelm
proper type for Library.using;
2016-10-11, by wenzelm
support user@host syntax;
2016-10-11, by wenzelm
modernized date format;
2016-10-11, by wenzelm
tuned signature;
2016-10-11, by wenzelm
eliminated extra trim_line: Process_Result.out/err are based on cat_lines, without trailing newline;
2016-10-11, by wenzelm
support for remote tmp dirs;
2016-10-11, by wenzelm
close more thoroughly;
2016-10-10, by wenzelm
provide execute operation, similar to Isabelle_System.bash;
2016-10-10, by wenzelm
proper support for exec channel (see also bash.scala);
2016-10-10, by wenzelm
proper hierarchic names;
2016-10-10, by wenzelm
more Sftp operations;
2016-10-10, by wenzelm
more specific channels;
2016-10-10, by wenzelm
clarified treatment of options;
2016-10-10, by wenzelm
support for remote command execution;
2016-10-10, by wenzelm
tuned;
2016-10-10, by wenzelm
more generous timeout default (see also jEdit/FTP);
2016-10-10, by wenzelm
connect session by default;
2016-10-10, by wenzelm
clarified (hardwired!) default (see also jEdit/FTP);
2016-10-10, by wenzelm
tuned comment;
2016-10-10, by wenzelm
support for SSH in Isabelle/Scala;
2016-10-09, by wenzelm
invariance of domain
2016-10-10, by paulson
enforce detailed build log;
2016-10-09, by wenzelm
record heap sizes;
2016-10-09, by wenzelm
inline session ML statistics into main build log;
2016-10-09, by wenzelm
modernized;
2016-10-09, by wenzelm
build_history log files with formal meta info;
2016-10-08, by wenzelm
prefer explicit timezone offset for printing;
2016-10-08, by wenzelm
tuned;
2016-10-08, by wenzelm
tuned name of bit truncating operations
2016-10-08, by haftmann
dedicated syntax for types with a length
2016-10-08, by haftmann
merged
2016-10-08, by wenzelm
prefer local timezone;
2016-10-08, by wenzelm
support for Isabelle/Jenkins log file format;
2016-10-08, by wenzelm
tuned;
2016-10-08, by wenzelm
clarified meta info;
2016-10-08, by wenzelm
tuned comment;
2016-10-08, by wenzelm
tuned signature;
2016-10-08, by wenzelm
tuned signature;
2016-10-08, by wenzelm
more permissive: accept all historic isatest and afp-test logs;
2016-10-08, by wenzelm
accept spurious empty logs;
2016-10-08, by wenzelm
prefer static Date_Format;
2016-10-08, by wenzelm
more formal directory content;
2016-10-08, by wenzelm
tuned error;
2016-10-08, by wenzelm
tuned;
2016-10-08, by wenzelm
misc tuning and clarification;
2016-10-08, by wenzelm
clarifying NEWS file
2016-10-08, by fleury
more flexible date formats;
2016-10-07, by wenzelm
support for isatest format;
2016-10-07, by wenzelm
tuned;
2016-10-07, by wenzelm
merged
2016-10-07, by wenzelm
accept obscure timezone used in 2011;
2016-10-07, by wenzelm
more liberal parsing for old AFP logs;
2016-10-07, by wenzelm
more operations;
2016-10-07, by wenzelm
more permissive timing data;
2016-10-07, by wenzelm
more permissive for old logs;
2016-10-07, by wenzelm
more uniform regexps;
2016-10-07, by wenzelm
clarified status: started sessions may bomb without explicit FAILED or CANCELLED (cf. in afp-test-devel-2016-01-03.log);
2016-10-07, by wenzelm
clarified parse_build_info: isabelle build output;
2016-10-07, by wenzelm
more operations;
2016-10-07, by wenzelm
more operations;
2016-10-07, by wenzelm
clarified signature;
2016-10-07, by wenzelm
more uniform treatment of settings;
2016-10-07, by wenzelm
clarified modules;
2016-10-07, by wenzelm
tuned;
2016-10-07, by wenzelm
more official legacy status;
2016-10-07, by wenzelm
more lemmas
2016-10-07, by fleury
tuning multisets
2016-10-07, by fleury
more lemmas
2016-10-07, by fleury
Set_Permutations -> Multiset_Permutations in NEWS
2016-10-07, by eberlm
moved to proper release (cf. 4a72b37ac4b8);
2016-10-07, by wenzelm
updated for release;
2016-10-07, by wenzelm
merged
2016-10-07, by wenzelm
Added tag Isabelle2016-1-RC0 for changeset 666c7475f4f7
2016-10-06, by wenzelm
merged
2016-10-06, by traytel
merged
2016-10-06, by traytel
less aggressive unfolding in tactic
2016-10-06, by traytel
merged
2016-10-06, by nipkow
moved lemmas
2016-10-06, by nipkow
merged
2016-10-06, by wenzelm
tuned signature;
2016-10-06, by wenzelm
misc tuning and clarification;
2016-10-06, by wenzelm
some support for header and data fields, notably from afp-test;
2016-10-05, by wenzelm
tuned signature;
2016-10-05, by wenzelm
more flexibile formatting;
2016-10-05, by wenzelm
proper calculation;
2016-10-05, by wenzelm
more operations;
2016-10-05, by wenzelm
more date and time operations from Java 8;
2016-10-05, by wenzelm
proper imports;
2016-10-05, by wenzelm
clarified modules;
2016-10-05, by wenzelm
more operations;
2016-10-05, by wenzelm
added multicore_base option;
2016-10-05, by wenzelm
allow multiple threads configurations;
2016-10-05, by wenzelm
tuned;
2016-10-05, by wenzelm
misc tuning and clarification;
2016-10-05, by wenzelm
clean output dir for fresh rebuild;
2016-10-05, by wenzelm
allow multiline script;
2016-10-05, by wenzelm
clarified sanity checks;
2016-10-05, by wenzelm
clarified modules;
2016-10-04, by wenzelm
historic workaround according to 22630327408b;
2016-10-04, by wenzelm
more thorought update of components;
2016-10-04, by wenzelm
check session name;
2016-10-04, by wenzelm
tuned signature;
2016-10-04, by wenzelm
tuned error;
2016-10-04, by wenzelm
earlier build_history_base: timing properties in log are introduced here;
2016-10-04, by wenzelm
incremental output;
2016-10-04, by wenzelm
clarified output;
2016-10-04, by wenzelm
clarified heap options;
2016-10-04, by wenzelm
proper ISABELLE_TOOL_JAVA_OPTIONS (as in "isabelle" wrapper);
2016-10-04, by wenzelm
more ambitious default as in former isatest;
2016-10-04, by wenzelm
tuned signature;
2016-10-04, by wenzelm
tuned;
2016-10-04, by wenzelm
more sanity checks;
2016-10-04, by wenzelm
more options for generated settings;
2016-10-04, by wenzelm
more robust build_history_base;
2016-10-03, by wenzelm
more robust;
2016-10-03, by wenzelm
proper log output;
2016-10-03, by wenzelm
clarified command line;
2016-10-03, by wenzelm
clarified command-line;
2016-10-03, by wenzelm
more operations;
2016-10-03, by wenzelm
more formal build_history_base;
2016-10-03, by wenzelm
clarified cold-start environment;
2016-10-03, by wenzelm
basic setup for Admin/build_history -- outside of Isabelle environment;
2016-10-03, by wenzelm
clarified: a variant of -i is the default, but its output is not as precise as it might seem;
2016-10-03, by wenzelm
merged
2016-10-05, by nipkow
replaced floorlog by floor/ceiling(log .)
2016-10-05, by nipkow
more multiset simp rules
2016-10-05, by fleury
tuned proof -- much faster
2016-10-05, by fleury
proof of concept for algebraically founded word types
2016-10-03, by haftmann
more lemmas
2016-10-03, by haftmann
option to report results of solve_direct as explicit warnings
2016-10-03, by haftmann
modernized option
2016-10-03, by haftmann
CONTRIBUTORS
2016-10-03, by haftmann
Probability: move some theorems from AFP/Density_Compiler
2016-10-03, by hoelzl
Probability: variant of central limit theorem with non-zero mean
2016-10-03, by hoelzl
HOL-Probability: more about probability, prepare for Markov processes in the AFP
2016-09-30, by hoelzl
Merge
2016-10-03, by paulson
new theorems including the theory FurtherTopology
2016-10-03, by paulson
clarified magic values (see also java/io/BufferedInputStream.java);
2016-10-03, by wenzelm
clarified stream operations;
2016-10-03, by wenzelm
tuned signature;
2016-10-03, by wenzelm
clarified modules;
2016-10-03, by wenzelm
more general read_stream: return actual byte count;
2016-10-03, by wenzelm
clarified modules;
2016-10-02, by wenzelm
more operations;
2016-10-02, by wenzelm
more operations;
2016-10-02, by wenzelm
more formal Mercurial support (with the potential to upgrade to command server);
2016-10-02, by wenzelm
tuned whitespace;
2016-10-02, by wenzelm
added isabelle_java cold-start executable;
2016-10-02, by wenzelm
updated according to 85c83757788c;
2016-10-02, by wenzelm
eliminated hard tabs;
2016-10-02, by wenzelm
updated headers;
2016-10-02, by wenzelm
updated to sumatra_pdf-3.1.2;
2016-10-02, by wenzelm
updated to xz-java-1.5;
2016-10-02, by wenzelm
updated cygwin according to 9416333a17c2, still using old 1.7.35-1;
2016-10-02, by wenzelm
tuned;
2016-10-02, by wenzelm
just one option is enough -- "isabelle jedit" java process may be prefixed directly in the shell;
2016-10-02, by wenzelm
options for process policy, notably for multiprocessor machines;
2016-10-01, by wenzelm
tuned;
2016-10-01, by wenzelm
tuned messages -- facilitate copy-paste;
2016-10-01, by wenzelm
merged
2016-10-01, by wenzelm
tuned;
2016-10-01, by wenzelm
tuned proofs;
2016-10-01, by wenzelm
Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
2016-10-01, by wenzelm
clarified lfp/gfp statements and proofs;
2016-10-01, by wenzelm
repair LaTeX
2016-10-01, by Lars Hupel
misc tuning for release;
2016-10-01, by wenzelm
added lemma;
2016-10-01, by wenzelm
Trying out "subgoal", and no more [| |]
2016-09-30, by paulson
HOL-Analysis: fix latex generation
2016-09-30, by hoelzl
Probability: fix proof
2016-09-30, by hoelzl
Library: fix name Product_plus to Product_Plus
2016-09-30, by hoelzl
HOL-Analysis: move Product_Vector and Inner_Product from Library
2016-09-30, by hoelzl
HOL-Analysis: move Continuum_Not_Denumerable from Library
2016-09-30, by hoelzl
HOL-Analysis: move Library/Convex to Convex_Euclidean_Space
2016-09-30, by hoelzl
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
2016-09-30, by hoelzl
new material on paths, etc. Also rationalisation
2016-09-30, by paulson
Merged
2016-09-30, by Manuel Eberl
Set_Permutations replaced by more general Multiset_Permutations
2016-09-29, by eberlm
CONTRIBUTORS: new proof method "argo"
2016-09-29, by boehmes
NEWS: new proof method "argo"
2016-09-29, by boehmes
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
2016-09-29, by boehmes
invoke argo as part of the tried automatic proof methods
2016-09-29, by boehmes
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
2016-09-29, by boehmes
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
2016-09-29, by hoelzl
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
2016-09-29, by hoelzl
HOL-Analysis: move gauges and (tagged) divisions to its own theory file
2016-09-29, by hoelzl
HOL-Analysis: add cover lemma ported by L. C. Paulson
2016-09-28, by hoelzl