Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+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.
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
more new material
2016-09-29, by paulson
Generalised the type of map_poly
2016-09-29, by paulson
Merge
2016-09-28, by paulson
new material connected with HOL Light measure theory, plus more rationalisation
2016-09-28, by paulson
sequential (jobs = 1) makeall profile
2016-09-28, by Lars Hupel
syntactic type class for operation mod named after mod;
2016-09-26, by haftmann
dropped tautological pattern
2016-09-26, by haftmann
more warning comments
2016-09-26, by haftmann
more lemmas
2016-09-26, by haftmann
spelling
2016-09-26, by haftmann
a few new theorems and a renaming
2016-09-27, by paulson
use filter to define Henstock-Kurzweil integration
2016-09-26, by hoelzl
include generation time in statistics
2016-09-24, by Lars Hupel
CI script to generate timing statistics
2016-09-24, by Lars Hupel
move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral
2016-09-23, by hoelzl
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
2016-09-23, by hoelzl
Merge
2016-09-22, by paulson
More mainly topological results
2016-09-22, by paulson
merged
2016-09-22, by wenzelm
discontinued raw symbols;
2016-09-22, by wenzelm
raw control symbols are superseded by Latex.embed_raw;
2016-09-22, by wenzelm
\<^raw> output is intended for LaTeX;
2016-09-21, by wenzelm
more general mixfix delimiters;
2016-09-21, by wenzelm
more tight implementation of symbol explode operation (without support for raw symbols);
2016-09-21, by wenzelm
approximation: preprocessing for nat/int expressions
2016-09-21, by immler
provide more information on error
2016-09-21, by immler
approximation: rewrite for reduction to base expressions
2016-09-21, by immler
new material about topological concepts, etc
2016-09-21, by paulson
vector_add_divide_simps now a "named theorems" bundle
2016-09-21, by paulson
tuned -- fewer warnings;
2016-09-20, by wenzelm
avoid old SML90;
2016-09-20, by wenzelm
more generic algebraic lemmas
2016-09-18, by haftmann
NEWS: Normalized_Fraction.thy
2016-09-20, by eberlm
Merged
2016-09-20, by eberlm
Additions to permutations (contributed by Lukas Bulwahn)
2016-09-19, by eberlm
resolve the name clash of HOL/Library/FSet and HOL/Quotient_Examples/FSet
2016-09-19, by kuncar
# after multiset intersection and union symbol
2016-09-19, by fleury
left_distrib ~> distrib_right, right_distrib ~> distrib_left
2016-09-19, by fleury
tuned;
2016-09-19, by wenzelm
merged
2016-09-18, by wenzelm
tuned proofs;
2016-09-18, by wenzelm
merged
2016-09-18, by Lars Hupel
tuned
2016-09-18, by Lars Hupel
clarified notation: iterated quantifier is negated as one chunk;
2016-09-18, by wenzelm
tuned proofs;
2016-09-18, by wenzelm
tuned;
2016-09-18, by wenzelm
clarified notation;
2016-09-18, by wenzelm
support replicate_mset in multiset simproc
2016-09-18, by fleury
tuning multiset simproc
2016-09-18, by fleury
repair LaTeX dropout from f83ef97d8d7d
2016-09-17, by Lars Hupel
prefer abbreviation for trivial set conversion
2016-09-16, by haftmann
more lemmas
2016-09-16, by haftmann
merged
2016-09-16, by wenzelm
more symbols -- as in the printed document;
2016-09-16, by wenzelm
more symbols;
2016-09-16, by wenzelm
tuned proofs
2016-09-16, by Lars Hupel
misc updates;
2016-09-16, by wenzelm
merged
2016-09-16, by wenzelm
consolidate implicit use of gnutar, via somewhat fragile dynamic scoping within existing shell scripts;
2016-09-16, by wenzelm
merged
2016-09-16, by immler
Liminf/Limsup and filtermap
2016-09-15, by immler
benchmark doesn't need to build documents
2016-09-16, by Lars Hupel
benchmark profile runs on small worker now (6 cores)
2016-09-16, by Lars Hupel
merged
2016-09-16, by traytel
NEWS
2016-09-16, by traytel
merged
2016-09-16, by wenzelm
serious measurements require jobs = 1;
2016-09-16, by wenzelm
sessions that are relevant for routine timing measurements;
2016-09-16, by wenzelm
more uniform completion of short word: exclude single character prefix but include two chracter prefix (see also 31633e503c17);
2016-09-16, by wenzelm
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
2016-09-16, by hoelzl
new type for finite maps; use it in HOL-Probability
2016-09-15, by Lars Hupel
adapted to listsum -> sum_list
2016-09-15, by nipkow
merged
2016-09-15, by nipkow
renamed listsum -> sum_list, listprod ~> prod_list
2016-09-15, by nipkow
lots of new results about topology, affine dimension etc
2016-09-15, by paulson
Merge
2016-09-15, by paulson
simple new lemmas, mostly about sets
2016-09-15, by paulson
add add_eq_0_iff_both_eq_0 and zero_eq_add_iff_both_eq_0 to simp set
2016-09-15, by hoelzl
tuned;
2016-09-15, by wenzelm
merged
2016-09-14, by wenzelm
NEWS;
2016-09-14, by wenzelm
handle font-size events;
2016-09-14, by wenzelm
clarified GUI representation of replacement texts with zero or more abbrevs;
2016-09-14, by wenzelm
handle update events;
2016-09-14, by wenzelm
discontinued global etc/abbrevs;
2016-09-14, by wenzelm
added abbrevs panel;
2016-09-14, by wenzelm
tuned;
2016-09-14, by wenzelm
more robust;
2016-09-14, by wenzelm
maintain abbrevs in canonical reverse order;
2016-09-14, by wenzelm
tuned;
2016-09-14, by wenzelm
tuned;
2016-09-14, by wenzelm
ignore default output directory of 'build_stats' tool
2016-09-14, by Lars Hupel
don't expose internal construction in the coinduction rule for mutual coinductive predicates
2016-09-13, by traytel
union associates to the left
2016-09-13, by blanchet
reorganization, more funs and lemmas
2016-09-13, by nipkow
more lemmas
2016-09-13, by nipkow
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
2016-09-12, by blanchet
tuned;
2016-09-12, by wenzelm
tuned -- fewer warnings;
2016-09-12, by wenzelm
moved ML function
2016-09-12, by blanchet
NEWS
2016-09-12, by blanchet
strengthened tactic
2016-09-12, by blanchet
avoid warning triggered by code generator
2016-09-12, by blanchet
strengthened tactic
2016-09-12, by blanchet
prove 'set' property backward
2016-09-12, by blanchet
more robust multiset simproc
2016-09-12, by fleury
delete looping simp rule
2016-09-12, by fleury
merged
2016-09-12, by wenzelm
tuned proofs;
2016-09-12, by wenzelm
tuned proofs;
2016-09-11, by wenzelm
generalized code towards nonuniform (co)datatypes
2016-09-11, by blanchet
merged
2016-09-11, by nipkow
more simp rules
2016-09-11, by nipkow
strengthened tactics
2016-09-11, by blanchet
derive relator properties forward
2016-09-11, by blanchet
derive maps forward
2016-09-11, by blanchet
tuning
2016-09-11, by blanchet
tuning
2016-09-11, by blanchet
provide a mechanism for ensuring dead type variables occur in typedef if desired
2016-09-11, by blanchet
preserve order of dead variables
2016-09-11, by blanchet
tuning
2016-09-11, by blanchet
tuned proofs;
2016-09-11, by wenzelm
misc tuning and modernization;
2016-09-11, by wenzelm
misc tuning and modernization;
2016-09-11, by wenzelm
more simp
2016-09-10, by nipkow
msetsum -> set_mset, msetprod -> prod_mset
2016-09-09, by nipkow
More on balancing; renamed theory to Balance
2016-09-09, by nipkow
added lemmas
2016-09-09, by nipkow
option "checkpoint" helps to fine-tune global heap space management;
2016-09-08, by wenzelm
made it easier to catch 'empty datatype' exception
2016-09-08, by blanchet
export ML functions
2016-09-08, by blanchet
tuning
2016-09-08, by blanchet
minimal HTTP server;
2016-09-08, by wenzelm
merged
2016-09-07, by wenzelm
unfold_abs_def is enabled by default;
2016-09-07, by wenzelm
discontinued theory-local special syntax for lattice orderings
2016-09-07, by haftmann
keep locale lifting rules on the global level
2016-09-07, by haftmann
tuning
2016-09-07, by blanchet
exported ML functions + tuning
2016-09-07, by blanchet
refactoring
2016-09-07, by blanchet
refactoring
2016-09-07, by blanchet
refactoring
2016-09-07, by blanchet
tuned whitespace
2016-09-07, by blanchet
merged
2016-09-06, by wenzelm
more operations;
2016-09-06, by wenzelm
clarified proof: save 1-2s CPU time;
2016-09-06, by wenzelm
tuned;
2016-09-06, by wenzelm
strictly sequential abbrevs;
2016-09-06, by wenzelm
clarified obscure facts;
2016-09-05, by wenzelm
clarified modules;
2016-09-05, by wenzelm
clarified modules;
2016-09-05, by wenzelm
standardized alias;
2016-09-05, by wenzelm
export more ML functions
2016-09-06, by blanchet
generalized ML signature
2016-09-06, by blanchet
extended ML signature + refactored
2016-09-06, by blanchet
extended ML signature
2016-09-06, by blanchet
generalized code (subtly)
2016-09-06, by blanchet
tuned ML signature
2016-09-06, by blanchet
exported ML functions
2016-09-05, by blanchet
export ML function + tuning
2016-09-05, by blanchet
tuning multisets; more interpretations
2016-09-05, by fleury
clean argument of simp add
2016-09-05, by fleury
add_mset constructor in multisets
2016-09-05, by fleury
merged
2016-09-05, by wenzelm
more operations;
2016-09-05, by wenzelm
more operations;
2016-09-05, by wenzelm
support resource management;
2016-09-05, by wenzelm
clarified modules;
2016-09-05, by wenzelm
export more ML functions
2016-09-05, by blanchet
export more ML functions
2016-09-05, by blanchet
added warning
2016-09-05, by blanchet
tuned;
2016-09-04, by wenzelm
tuned signature;
2016-09-04, by wenzelm
clarified exceptions;
2016-09-04, by wenzelm
support for (single) primary key;
2016-09-04, by wenzelm
more operations;
2016-09-04, by wenzelm
more operations;
2016-09-04, by wenzelm
clarified modules;
2016-09-04, by wenzelm
tuned;
2016-09-03, by wenzelm
minimal support for SQLite databases;
2016-09-03, by wenzelm
merged
2016-09-02, by wenzelm
make double-sure that refresh happens eventually, even without edits (e.g. height change) -- amending 8bf765c9c2e5;
2016-09-02, by wenzelm
simplified;
2016-09-02, by wenzelm
tuned;
2016-09-02, by wenzelm
merged
2016-09-02, by nipkow
added lemmas
2016-09-02, by nipkow
consider equality proxy in monotonicity analysis
2016-09-02, by blanchet
adapted remote E
2016-09-02, by blanchet
Merged
2016-09-02, by Manuel Eberl
Some facts about factorial and binomial coefficients
2016-09-01, by Manuel Eberl
added inorder2
2016-09-02, by nipkow
tuned headers;
2016-09-01, by wenzelm
clarified session: use all theories in directory HOL/Library;
2016-09-01, by wenzelm
clarified session;
2016-09-01, by wenzelm
more careful quoting, e.g. relevant for \<^control>cartouche;
2016-09-01, by wenzelm
uniform capitalization of labels;
2016-09-01, by wenzelm
tuned message;
2016-09-01, by wenzelm
merged
2016-09-01, by wenzelm
avoid conflict after initial keymap migration;
2016-09-01, by wenzelm
merged
2016-09-01, by nipkow
Renamed balanced to complete; added balanced; more about both
2016-09-01, by nipkow
tuned GUI: modal dialog last;
2016-09-01, by wenzelm
tuned message;
2016-09-01, by wenzelm
merged
2016-09-01, by wenzelm
NEWS;
2016-09-01, by wenzelm
more robust persistent storage;
2016-09-01, by wenzelm
clarified important directories;
2016-09-01, by wenzelm
separate action;
2016-09-01, by wenzelm
check keymap changes on startup;
2016-09-01, by wenzelm
tuned message;
2016-09-01, by wenzelm
clarified GUI;
2016-09-01, by wenzelm
actual actions;
2016-09-01, by wenzelm
tuned;
2016-09-01, by wenzelm
clarified;
2016-09-01, by wenzelm
tuned GUI;
2016-09-01, by wenzelm
clarified GUI;
2016-08-31, by wenzelm
tuned GUI;
2016-08-31, by wenzelm
tuned rendering;
2016-08-31, by wenzelm
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
2016-08-31, by wenzelm
clarified shortcut conflicts;
2016-08-31, by wenzelm
clarified (see 019856db2bb6, ea52509f4c42);
2016-08-31, by wenzelm
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
2016-08-30, by wenzelm
added glyph from "Deja Vu Sans Mono" font;
2016-08-30, by wenzelm
more robustness
2016-09-01, by blanchet
added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
2016-09-01, by blanchet
make workaround possible for Quickcheck with nesting
2016-09-01, by blanchet
tuned docs
2016-08-30, by blanchet
tuned final stop in message
2016-08-30, by blanchet
generate proper goal when equation is entered programmatically
2016-08-30, by traytel
clarified default;
2016-08-29, by wenzelm
Bohr-Mollerup theorem for the Gamma function
2016-08-26, by Manuel Eberl
Back to original example theorem.
2016-08-25, by ballarin
Improved error reporting when activating a locale instance.
2016-08-25, by ballarin
Deprivatisation of lemmas in Polynomial_Factorial
2016-08-25, by Manuel Eberl
More analysis lemmas
2016-08-25, by Manuel Eberl
added lemma
2016-08-24, by nipkow
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
tip