2018-05-04 |
wenzelm |
no censorship of view title;
|
changeset |
files
|
2018-05-04 |
wenzelm |
set view title dynamically;
|
changeset |
files
|
2018-05-04 |
nipkow |
tuned
|
changeset |
files
|
2018-05-04 |
nipkow |
tuned
|
changeset |
files
|
2018-05-03 |
paulson |
Some tidying up (mostly regarding summations from 0)
|
changeset |
files
|
2018-05-03 |
paulson |
tidied up Infinite_Products
|
changeset |
files
|
2018-05-03 |
immler |
merged
|
changeset |
files
|
2018-05-03 |
immler |
fixed HOL-Analysis
|
changeset |
files
|
2018-05-03 |
immler |
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
|
changeset |
files
|
2018-05-02 |
immler |
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
|
changeset |
files
|
2018-05-03 |
paulson |
a lemma about infinite products
|
changeset |
files
|
2018-05-02 |
paulson |
merged
|
changeset |
files
|
2018-05-02 |
paulson |
tidying up and using real induction methods
|
changeset |
files
|
2018-05-02 |
wenzelm |
tuned -- slightly smaller future closure size;
|
changeset |
files
|
2018-05-02 |
wenzelm |
clarified menu actions;
|
changeset |
files
|
2018-05-02 |
wenzelm |
purge history more thoroughly (see also 3156faac30a7);
|
changeset |
files
|
2018-05-02 |
paulson |
merged
|
changeset |
files
|
2018-05-02 |
paulson |
type class generalisations; some work on infinite products
|
changeset |
files
|
2018-05-02 |
paulson |
merged
|
changeset |
files
|
2018-05-01 |
paulson |
simplified some messy proofs
|
changeset |
files
|
2018-05-01 |
wenzelm |
clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations);
|
changeset |
files
|
2018-05-01 |
wenzelm |
avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
|
changeset |
files
|
2018-04-30 |
paulson |
merged
|
changeset |
files
|
2018-04-30 |
paulson |
more general tidying up
|
changeset |
files
|
2018-04-30 |
boehmes |
prefer explicit error message to unspecific Options exception: Z3 proof traces may lack information necessary for replay when dealing with quantified formulas
|
changeset |
files
|
2018-04-29 |
paulson |
cleaned up more messy proofs
|
changeset |
files
|
2018-04-29 |
paulson |
more defer/prefer
|
changeset |
files
|
2018-04-28 |
paulson |
getting rid of more "defer", etc.
|
changeset |
files
|
2018-04-28 |
paulson |
getting rid of "defer"
|
changeset |
files
|
2018-04-27 |
paulson |
another big cleanup
|
changeset |
files
|
2018-04-27 |
paulson |
merged
|
changeset |
files
|
2018-04-27 |
paulson |
minor typeclass generalisations and junk removal
|
changeset |
files
|
2018-04-26 |
paulson |
merged
|
changeset |
files
|
2018-04-26 |
paulson |
more messy proofs
|
changeset |
files
|
2018-04-26 |
nipkow |
merged
|
changeset |
files
|
2018-04-26 |
nipkow |
new simp modifier: reorient
|
changeset |
files
|
2018-04-26 |
paulson |
small typeclass generalisations
|
changeset |
files
|
2018-04-26 |
paulson |
merged
|
changeset |
files
|
2018-04-26 |
paulson |
some of Jose Divasón's material from Rank_Nullity_Theorem/Miscellaneous
|
changeset |
files
|
2018-04-26 |
wenzelm |
spelling;
|
changeset |
files
|
2018-04-25 |
paulson |
more messy proofs redone, and new material
|
changeset |
files
|
2018-04-25 |
paulson |
merged
|
changeset |
files
|
2018-04-25 |
paulson |
merged
|
changeset |
files
|
2018-04-25 |
paulson |
new material on matricies by Tim Makarios (from Tarskis_Geometry in the AFP)
|
changeset |
files
|
2018-04-25 |
wenzelm |
merged
|
changeset |
files
|
2018-04-25 |
wenzelm |
tuned -- avoid spurious exception trace for "the";
|
changeset |
files
|
2018-04-25 |
haftmann |
proof of concept for residue rings over int using type numerals
|
changeset |
files
|
2018-04-25 |
haftmann |
more correct error message
|
changeset |
files
|
2018-04-25 |
haftmann |
uniform tagging for printable and non-printable literals
|
changeset |
files
|
2018-04-24 |
paulson |
merged
|
changeset |
files
|
2018-04-24 |
paulson |
fixing more messy proofs
|
changeset |
files
|
2018-04-24 |
wenzelm |
more ambitious parallelism (in contrast to a8ee8e4884ec): pri = 1 ensures that internal proof tasks are executed before the already forked theory outline with pri = 0;
|
changeset |
files
|
2018-04-24 |
wenzelm |
eliminated pointless special case (see also a8ee8e4884ec, c4c4c2f01723);
|
changeset |
files
|
2018-04-24 |
haftmann |
proper datatype for 8-bit characters
|
changeset |
files
|
2018-04-24 |
haftmann |
corrected nonsense
|
changeset |
files
|
2018-04-24 |
wenzelm |
less ambitious parallelism: avoid problems with HOL-Proofs and threads=2 (congestion with many thousands futures and rather dense heap);
|
changeset |
files
|
2018-04-24 |
wenzelm |
clarified modules;
|
changeset |
files
|
2018-04-23 |
paulson |
tidied some horrid proofs
|
changeset |
files
|
2018-04-23 |
nipkow |
del_max -> split_max
|
changeset |
files
|
2018-04-22 |
paulson |
Tidied a lot of messy proofs
|
changeset |
files
|
2018-04-21 |
nipkow |
dont rename PQ.del_min
|
changeset |
files
|
2018-04-21 |
nipkow |
del_min -> split_min
|
changeset |
files
|
2018-04-20 |
wenzelm |
merged
|
changeset |
files
|
2018-04-20 |
wenzelm |
support for XZ.Cache;
|
changeset |
files
|