isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 tip

merged
2017-10-30, by paulson
New results in topology, mostly from HOL Light's moretop.ml
2017-10-30, by paulson
generalized some lemmas on multisets
2017-10-30, by haftmann
rule out pathologic instances
2017-10-30, by haftmann
tuned some proofs and added some lemmas
2017-10-30, by haftmann
more recent polyml-test version;
2017-10-29, by wenzelm
reduced simp_depth_limit
2017-10-29, by nipkow
generalized
2017-10-28, by immler
reduced heap hierarchy, for potentially improved performance;
2017-10-28, by wenzelm
deactivated old tests;
2017-10-28, by wenzelm
avoid slow proofs due to simp rules from 960509bfd47e;
2017-10-28, by wenzelm
some concrete commands;
2017-10-27, by wenzelm
tuned signature;
2017-10-27, by wenzelm
more formal messages;
2017-10-27, by wenzelm
tuned signature;
2017-10-27, by wenzelm
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
2017-10-27, by wenzelm
more permissive;
2017-10-27, by wenzelm
tuned;
2017-10-27, by wenzelm
separate JSON lexer;
2017-10-26, by wenzelm
clarified command language;
2017-10-26, by wenzelm
use Poly/ML 5.7.1 test version as default;
2017-10-26, by wenzelm
more explicit check;
2017-10-25, by wenzelm
more robust treatment of UTF8 in raw byte sources;
2017-10-25, by wenzelm
clarified check, assuming that load commands are plain ASCII;
2017-10-25, by wenzelm
more documentation;
2017-10-25, by wenzelm
disallow blanks, relevant for session_name / theory_name e.g. in build log files;
2017-10-25, by wenzelm
uniform system name;
2017-10-25, by wenzelm
store session sources stamp;
2017-10-24, by wenzelm
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
2017-10-24, by immler
misc tuning and modernization;
2017-10-24, by wenzelm
tuned output;
2017-10-24, by wenzelm
discontinued Linux 32bit platform support;
2017-10-23, by wenzelm
obsolete;
2017-10-23, by wenzelm
merged
2017-10-23, by wenzelm
updated to jdk-8u152, which is for x86_64 only;
2017-10-23, by wenzelm
added lemma
2017-10-23, by nipkow
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
2017-10-23, by wenzelm
tuned output;
2017-10-22, by wenzelm
updated test version;
2017-10-22, by wenzelm
merged
2017-10-22, by wenzelm
auto update;
2017-10-22, by wenzelm
more recent polyml-test version;
2017-10-22, by wenzelm
parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
2017-10-22, by wenzelm
tuned;
2017-10-22, by wenzelm
clarified signature;
2017-10-22, by wenzelm
tuned: build hg_graph only once;
2017-10-22, by wenzelm
tuned
2017-10-22, by nipkow
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
2017-10-22, by nipkow
remove trailing whitespaces in List
2017-10-21, by bulwahn
drop a superfluous assumption that was found by the find_unused_assms command
2017-10-21, by bulwahn
drop a superfluous assumption that was found by the find_unused_assms command and tune proof
2017-10-21, by bulwahn
drop a superfluous assumption that was found by the find_unused_assms command and tune proof
2017-10-21, by bulwahn
algebraic foundation for congruences
2017-10-20, by haftmann
more ambitious test;
2017-10-20, by wenzelm
added lemmas and tuned proofs
2017-10-20, by haftmann
merged
2017-10-19, by paulson
Switching to inverse image and constant_on, plus some new material
2017-10-19, by paulson
proper integer option for Admin/build_history;
2017-10-19, by wenzelm
clarified output;
2017-10-18, by wenzelm
tuned output;
2017-10-18, by wenzelm
more thorough treatment of afp_version and afp_pull_date;
2017-10-18, by wenzelm
tuned options;
2017-10-18, by wenzelm
tuned output;
2017-10-17, by wenzelm
uniform execute, with proper isabelle_identifier (notably for "isabelle components -I");
2017-10-17, by wenzelm
tuned;
2017-10-17, by wenzelm
permissive theory_timings for historic versions;
2017-10-17, by wenzelm
store theory timings in session in build_log database;
2017-10-16, by wenzelm
provide theory timing information, similar to command timing but always considered relevant;
2017-10-16, by wenzelm
tuned;
2017-10-16, by wenzelm
init user settings on fresh test machine;
2017-10-16, by wenzelm
added [simp]
2017-10-16, by nipkow
proper value;
2017-10-15, by wenzelm
more AFP tests;
2017-10-15, by wenzelm
added ml_statistics_step to trim stored properties;
2017-10-15, by wenzelm
proper argument;
2017-10-15, by wenzelm
tuned (graph.all_succs already contains origin);
2017-10-14, by wenzelm
support for AFP versions;
2017-10-14, by wenzelm
clarified afp_pull_date: both repository versions are relevant;
2017-10-14, by wenzelm
clarified stored build_args;
2017-10-14, by wenzelm
partition AFP sessions according to structure, which happens to cut it roughly into equal parts;
2017-10-14, by wenzelm
support for AFP in build_history and remote_build_history;
2017-10-14, by wenzelm
tuned whitespace;
2017-10-13, by wenzelm
support for AFP versions;
2017-10-13, by wenzelm
tuned signature;
2017-10-13, by wenzelm
tuned signature;
2017-10-13, by wenzelm
support for AFP versions;
2017-10-13, by wenzelm
tuned;
2017-10-13, by wenzelm
added lemmas, tuned spaces
2017-10-13, by nipkow
entries_graph requires acyclic graph, but lazy val allows forming the AFP object nonetheless;
2017-10-12, by wenzelm
more informative Imports.Report with actual session imports (minimized);
2017-10-12, by wenzelm
more robust: allow URLs;
2017-10-12, by wenzelm
more robust: allow Windows file names;
2017-10-12, by wenzelm
clarified signature;
2017-10-12, by wenzelm
relaxed assm
2017-10-12, by nipkow
back to build_polyml_component according to 54c6ec4166a4 (amending 808e6ddb5a50);
2017-10-11, by wenzelm
reactivated unfinished tool (cf. a3a847c4fbdb);
2017-10-11, by wenzelm
tuned whitespace;
2017-10-11, by wenzelm
clarified meta_digest;
2017-10-11, by wenzelm
tuned;
2017-10-11, by wenzelm
added isablle build option -f;
2017-10-11, by wenzelm
canonical multiplicative euclidean size
2017-10-09, by haftmann
clarified parity
2017-10-09, by haftmann
clarified uniqueness criterion for euclidean rings
2017-10-09, by haftmann
tuned proofs
2017-10-09, by haftmann
tuned imports
2017-10-09, by haftmann
fixed markup
2017-10-10, by paulson
ignore isolated nodes by default;
2017-10-10, by wenzelm
merged
2017-10-10, by wenzelm
cycle check with informative error;
2017-10-10, by wenzelm
tuned: each session has at most one defining entry;
2017-10-10, by wenzelm
more operations;
2017-10-10, by wenzelm
tuned signature;
2017-10-10, by wenzelm
tuned signature;
2017-10-10, by wenzelm
Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
2017-10-10, by paulson
Session HOL-Analysis: Moebius functions and the Riemann mapping theorem.
2017-10-10, by paulson
merged
2017-10-09, by wenzelm
tuned: less oo-non-sense;
2017-10-09, by wenzelm
operations for graph display;
2017-10-09, by wenzelm
tuned signature;
2017-10-09, by wenzelm
dependencies of entries vs. sessions;
2017-10-09, by wenzelm