Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-224
+224
+1000
+3000
+10000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
tuned signature;
2018-02-20, by wenzelm
fixed the proof of pair_measure_count_space
2018-02-23, by paulson
merged
2018-02-23, by paulson
fixing ennreal using add_mono1; shifting results from linordered_semidom to linordered_nonzero_semiring
2018-02-23, by paulson
merged
2018-02-22, by paulson
type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0
2018-02-22, by paulson
simplified Radix_Sort
2018-02-23, by nipkow
merged
2018-02-22, by immler
merged
2018-02-22, by immler
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
2018-02-22, by immler
simplified def of stable
2018-02-22, by nipkow
Lots of new material about matrices, etc.
2018-02-21, by paulson
tuned proofs -- prefer explicit names for facts from 'interpret';
2018-02-20, by wenzelm
merged
2018-02-20, by wenzelm
eliminated questionable Par_List.map -- locale interpretation is mostly lazy (see also b81f1de9f57e);
2018-02-20, by wenzelm
tuned signature;
2018-02-20, by wenzelm
tuned;
2018-02-20, by wenzelm
use lazy notes for locale context init and later additions of facts;
2018-02-20, by wenzelm
avoid premature Lazy.force due to strict "?" operator;
2018-02-20, by wenzelm
Merge
2018-02-20, by paulson
Merge
2018-02-19, by paulson
lots of new material, ultimately related to measure theory
2018-02-19, by paulson
merged
2018-02-19, by wenzelm
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
2018-02-19, by wenzelm
tuned;
2018-02-19, by wenzelm
tuned: more parallel;
2018-02-19, by wenzelm
clarified modules;
2018-02-19, by wenzelm
clarified modules;
2018-02-19, by wenzelm
tuned;
2018-02-19, by wenzelm
tuned;
2018-02-19, by wenzelm
tuned signature;
2018-02-19, by wenzelm
tuned: more accurate transfer;
2018-02-19, by wenzelm
store facts as lazy values;
2018-02-19, by wenzelm
clarified operations;
2018-02-19, by wenzelm
misc tuning and clarification;
2018-02-19, by wenzelm
clarified signature;
2018-02-19, by wenzelm
clarified modules;
2018-02-19, by wenzelm
more operations;
2018-02-19, by wenzelm
added lemma
2018-02-19, by nipkow
tuned;
2018-02-18, by wenzelm
clarified signature;
2018-02-18, by wenzelm
misc tuning and clarification;
2018-02-18, by wenzelm
clarified signature;
2018-02-18, by wenzelm
more explicit instantiate_morphism (without checks for typ / term component);
2018-02-18, by wenzelm
tuned;
2018-02-18, by wenzelm
tuned signature;
2018-02-18, by wenzelm
more thorough jEdit.propertiesChanged(), which includes KeymapManager.reload() and jEdit.initKeyBindings();
2018-02-17, by wenzelm
avoid conflict with Isabelle/jEdit completion of '>', e.g. "-->", "==>";
2018-02-17, by wenzelm
trim context of persistent data;
2018-02-17, by wenzelm
trim context of persistent data;
2018-02-17, by wenzelm
trim context of persistent data;
2018-02-17, by wenzelm
clarified apply_transaction: always continue without presentation context;
2018-02-17, by wenzelm
more tight presentation context: avoid storing full Toplevel.state;
2018-02-17, by wenzelm
tuned;
2018-02-17, by wenzelm
more informative theories_trace;
2018-02-17, by wenzelm
merged
2018-02-17, by wenzelm
tuned signature (again);
2018-02-16, by wenzelm
trim context of persistent data;
2018-02-16, by wenzelm
trim context of persistent data;
2018-02-16, by wenzelm
proper file name;
2018-02-16, by wenzelm
trim context of persistent data;
2018-02-16, by wenzelm
clarified data operations, with trim_context and transfer;
2018-02-16, by wenzelm
tuned;
2018-02-16, by wenzelm
trim context of persistent data;
2018-02-16, by wenzelm
trim context of persistent data;
2018-02-16, by wenzelm
removed unused material;
2018-02-16, by wenzelm
trim context of persistent data;
2018-02-16, by wenzelm
trim context of persistent data;
2018-02-16, by wenzelm
tuned;
2018-02-16, by wenzelm
tuned whitespace;
2018-02-16, by wenzelm
more operations;
2018-02-16, by wenzelm
optional trace of created theory values;
2018-02-16, by wenzelm
more operations;
2018-02-16, by wenzelm
auxiliary operation for space profiling;
2018-02-15, by wenzelm
special treatment of 0 only refers to type char
2018-02-03, by haftmann
merged
2018-02-16, by Lars Hupel
features and caveats of datatype_record
2018-02-16, by Lars Hupel
merged
2018-02-16, by Andreas Lochbihler
strengthen filter relator to canonical categorical definition with better properties
2018-02-16, by Andreas Lochbihler
recovered outer Pretty.block from 30c1639a343a, avoid excessive line breaks due to implicit Pretty.chunks;
2018-02-15, by wenzelm
merged
2018-02-15, by wenzelm
more symbols;
2018-02-15, by wenzelm
New theory ex/Radix_Sort.thy
2018-02-14, by nipkow
records based on datatypes/BNF infrastructure
2018-02-14, by Lars Hupel
updated polyml component;
2018-02-13, by wenzelm
no --enable-shared: leads to slow bigint operations (e.g. in session HOL-ODE-Examples);
2018-02-13, by wenzelm
retain remote_builds_old for build_status;
2018-02-13, by wenzelm
lxbroy7 no longer exists;
2018-02-13, by wenzelm
added lemmas
2018-02-12, by nipkow
corrected some URLs
2018-02-12, by Lars Hupel
permissive Doc.dirs: some entries may be absent due to distribution bootstrap, e.g. $JEDIT_HOME/dist/doc;
2018-02-12, by wenzelm
merged
2018-02-11, by wenzelm
updated polyml component -- omitting bad polyml-5.7.1-3;
2018-02-11, by wenzelm
use preferred resolver according to DOI Handbook ยง3.8
2018-02-11, by Lars Hupel
no --enable-shared for x86_64-darwin: does not work on some test machine;
2018-02-11, by wenzelm
proper target directory;
2018-02-11, by wenzelm
tuned;
2018-02-11, by wenzelm
more robust options;
2018-02-11, by wenzelm
back to --disable-shared on windows to avoid odd core-dump of polyimport;
2018-02-11, by wenzelm
tuned;
2018-02-11, by wenzelm
back to --disable-shared on x86-darwin to avoid odd core-dump of polyimport;
2018-02-11, by wenzelm
clarified command-line defaults;
2018-02-11, by wenzelm
enforce shared libpoly on all platforms, with File.copy before File.move;
2018-02-11, by wenzelm
NEWS;
2018-02-10, by wenzelm
updated to polyml-5.7.1-2, which includes libgmp for x86-darwin as well;
2018-02-10, by wenzelm
support for libgmp for x86-darwin;
2018-02-10, by wenzelm
more accessible src/Pure/ROOT.ML;
2018-02-10, by wenzelm
tuned;
2018-02-10, by wenzelm
more robust: avoid global change of LD_LIBRARY_PATH (e.g. relevant for subprocesses);
2018-02-09, by wenzelm
rebuild of polyml-5.7.1 with libgmp for x86_darwin;
2018-02-09, by wenzelm
patch polyc: avoid hardwired directory prefix;
2018-02-09, by wenzelm
support for libgmp for x86_64-darwin;
2018-02-09, by wenzelm
built-in library path for (optional) libgmp on macos;
2018-02-09, by wenzelm
removed obsolete polyi executable: change of DYLD_LIBRARY_PATH is not required;
2018-02-09, by wenzelm
more robust access to shared libraries for poly executable: avoid global change of LD_LIBRARY_PATH (e.g. relevant for subprocesses);
2018-02-09, by wenzelm
Merged
2018-02-08, by eberlm
Some lemmas about complex sinh/cosh/tanh
2018-02-08, by Manuel Eberl
more elementary proof of connected_Times, earlier
2018-02-08, by immler
merged
2018-02-08, by nipkow
tuned
2018-02-08, by nipkow
Added hyperbolic functions
2018-02-07, by eberlm
added lemmas, avoid 'float_of 0'
2018-02-05, by immler
clarified signature;
2018-02-03, by wenzelm
more uniform treatment of formal comments within document source;
2018-02-03, by wenzelm
just one check of formal comments;
2018-02-03, by wenzelm
avoid proliferation of language_document reports;
2018-02-03, by wenzelm
more external tools for AFP test;
2018-02-03, by wenzelm
clarified overall range: include delimiters;
2018-02-03, by wenzelm
added lemma
2018-02-02, by nipkow
tuned: more standard use of order;
2018-02-01, by wenzelm
tuned;
2018-02-01, by wenzelm
tuned;
2018-02-01, by wenzelm
clarified signature;
2018-02-01, by wenzelm
clarified signature: prefer proper order operation;
2018-02-01, by wenzelm
tuned signature: more operations;
2018-02-01, by wenzelm
clarified signature;
2018-02-01, by wenzelm
proper term_ord as in HOL/Library/positivstellensatz.ML, e.g. relevant for "0 <= c & 0 <= a ==> a + bb = 1 & c <= 1 ==> bb * c * 4 <= (12::real)";
2018-01-31, by wenzelm
performance fine-tuning of hot spot;
2018-01-31, by wenzelm
tuned;
2018-01-31, by wenzelm
more efficient tokens_match_ord based on token_kind_index;
2018-01-31, by wenzelm
more abstract type;
2018-01-31, by wenzelm
tuned;
2018-01-31, by wenzelm
clarified signature;
2018-01-31, by wenzelm
clarified signature;
2018-01-31, by wenzelm
explicit dummy token;
2018-01-31, by wenzelm
clarified modules;
2018-01-31, by wenzelm
clarified signature;
2018-01-31, by wenzelm
clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;
2018-01-30, by wenzelm
clarified lines: like split_lines;
2018-01-30, by wenzelm
tuned;
2018-01-30, by wenzelm
unused;
2018-01-30, by wenzelm
tuned;
2018-01-30, by wenzelm
simplified: prod_count is always NONE;
2018-01-30, by wenzelm
tuned;
2018-01-30, by wenzelm
tuned data structure and operations;
2018-01-30, by wenzelm
tuned data structure and operations;
2018-01-30, by wenzelm
tuned data structure and operations;
2018-01-30, by wenzelm
more operations;
2018-01-30, by wenzelm
prefer specific tokens_subtract: subtle change of comparison via tokens_match;
2018-01-30, by wenzelm
tuned type: absorb NONE: token option as token_none: token;
2018-01-30, by wenzelm
tuned;
2018-01-30, by wenzelm
clarified types and operations: potentially more efficient add_prods;
2018-01-30, by wenzelm
clarified modules;
2018-01-30, by wenzelm
tuned: more explicit types;
2018-01-30, by wenzelm
tuned data structure: potentially more efficient add_prods;
2018-01-29, by wenzelm
clarified operations;
2018-01-29, by wenzelm
merged
2018-01-29, by wenzelm
expand definitions of \DeclareOldFontCommand in traditional article.cls, e.g. KOMA-Script no longer provides these;
2018-01-29, by wenzelm
irrelevant reference to doubtful theory Code_Char
2018-01-29, by haftmann
avoid concrete (anti)mono in theorem names since it could be the other way round
2018-01-28, by haftmann
more uniform documentation;
2018-01-29, by wenzelm
proper fall-back rendering of control symbol;
2018-01-29, by wenzelm
clarified take/drop/chop prefix/suffix;
2018-01-28, by wenzelm
clarified signature;
2018-01-28, by wenzelm
proper signature (amending c4e9e0c50487);
2018-01-28, by wenzelm
tuned output;
2018-01-27, by wenzelm
tuned;
2018-01-27, by wenzelm
explicit graph for chains, which contains all nts as nodes;
2018-01-27, by wenzelm
tuned;
2018-01-27, by wenzelm
tuned;
2018-01-27, by wenzelm
prefer lazy update;
2018-01-27, by wenzelm
tuned output;
2018-01-27, by wenzelm
more operations;
2018-01-27, by wenzelm
include lemmas generally useful for combinatorial proofs
2018-01-27, by bulwahn
redundant;
2018-01-26, by wenzelm
allow cartouche within ML string;
2018-01-25, by wenzelm
verbatim output consists of plain lines;
2018-01-25, by wenzelm
old-style inner comments are legacy;
2018-01-25, by wenzelm
more markup: disable spell-checker for raw latex;
2018-01-25, by wenzelm
clarified signature: items with \isasep are special;
2018-01-25, by wenzelm
clarified signature;
2018-01-25, by wenzelm
tuned message;
2018-01-25, by wenzelm
clarified operations;
2018-01-24, by wenzelm
tuned signature: removed unused operations;
2018-01-24, by wenzelm
tuned: prefer list operations over Source.source;
2018-01-24, by wenzelm
tuned: prefer list operations over Source.source;
2018-01-24, by wenzelm
tuned: prefer list operations over Source.source;
2018-01-24, by wenzelm
clarified signature;
2018-01-24, by wenzelm
clarified position;
2018-01-24, by wenzelm
clarified operations;
2018-01-24, by wenzelm
merged
2018-01-23, by wenzelm
treat sessions as entities with defining position;
2018-01-23, by wenzelm
options file for x86_64 only (amending 03a96b8c7c06);
2018-01-23, by wenzelm
updated to jdk-8u162;
2018-01-23, by wenzelm
more robust java.ext.dirs: avoid picking up accidental jars from system directories;
2018-01-23, by wenzelm
drop redundant cong rules
2018-01-23, by Lars Hupel
merged
2018-01-22, by Lars Hupel
drop redundant fundef_cong rule
2018-01-22, by Lars Hupel
tuned
2018-01-22, by Lars Hupel
repair malformed fundef_cong rule
2018-01-22, by Lars Hupel
removed duplicate
2018-01-22, by nipkow
tuned message: same error may occur in different contexts;
2018-01-22, by wenzelm
detect more errors;
2018-01-21, by wenzelm
merged
2018-01-21, by nipkow
made sorted fun again
2018-01-21, by nipkow
imported patch sorted
2018-01-20, by nipkow
add lemma on lists from Falling_Factorial_Sum entry
2018-01-20, by bulwahn
merged
2018-01-19, by wenzelm
avoid evaluation of embedded comment;
2018-01-19, by wenzelm
disable "display" style in marginal (line) comment;
2018-01-19, by wenzelm
more uniform output of source / text / theory_text, with handling of formal comments etc.;
2018-01-19, by wenzelm
sort completion result;
2018-01-19, by wenzelm
recovered antiquotation check without latex mode (cf. dfc93f2b01ea);
2018-01-19, by wenzelm
formal treatment of documentation names;
2018-01-19, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-224
+224
+1000
+3000
+10000
tip