isabelle: Graph

upgraded CVC4 component to fix abnormal termination reported by Larry Paulson
2017-08-24, by blanchet
dedicated local for "operative" avoids namespace pollution
2017-08-23, by haftmann
reorg
2017-08-23, by nipkow
added lemma
2017-08-23, by nipkow
Merged
2017-08-23, by eberlm
HOL-Library: going_to filter
2017-08-23, by Manuel Eberl
more on the dreadful monotone_convergence_interval
2017-08-23, by paulson
Lemmas about analysis and permutations
2017-08-22, by Manuel Eberl
tuned
2017-08-22, by Lars Hupel
merged
2017-08-22, by Lars Hupel
tuned syntax
2017-08-22, by Lars Hupel
tuned;
2017-08-22, by wenzelm
output syntax for pattern aliases
2017-08-22, by Lars Hupel
HOL-Analysis: Convergent FPS and infinite sums
2017-08-21, by Manuel Eberl
proper argument type (amending 8d5cb4ea2b7c);
2017-08-21, by wenzelm
tuned;
2017-08-21, by wenzelm
updated for release;
2017-08-21, by wenzelm
tuned;
2017-08-21, by wenzelm
misc updates for release;
2017-08-21, by wenzelm
tuned;
2017-08-21, by wenzelm
tuned;
2017-08-21, by wenzelm
misc tuning and updates for release;
2017-08-21, by wenzelm
updated to sqlite-jdbc-3.20.0;
2017-08-21, by wenzelm
updated to postgresql-42.1.4;
2017-08-21, by wenzelm
avoid compound edit: it causes confusion about the context of the last line, e.g. final "end";
2017-08-21, by wenzelm
added missing file (cf. 9098c36abd1a);
2017-08-21, by wenzelm
Merged
2017-08-20, by Manuel Eberl
More lemmas for HOL-Analysis
2017-08-20, by Manuel Eberl
merged
2017-08-20, by wenzelm
updated for release;
2017-08-20, by wenzelm
enforce Isabelle plugins to be enabled;
2017-08-20, by wenzelm
officially allow restart of Isabelle plugin;
2017-08-20, by wenzelm
reinit the manager thread, e.g. after restart of the Isabelle/jEdit plugin;
2017-08-20, by wenzelm
proper update of options (amending c3d6dd17d626);
2017-08-20, by wenzelm
more robust plugin restart;
2017-08-20, by wenzelm
more robust shutdown, e.g. when plugin is stopped;
2017-08-20, by wenzelm
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
2017-08-20, by wenzelm
Various lemmas for HOL-Analysis
2017-08-20, by Manuel Eberl
merged
2017-08-18, by wenzelm
more NEWS;
2017-08-18, by wenzelm
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2017-08-18, by wenzelm
more informative error message, e.g. relevant for incoherent imports;
2017-08-18, by wenzelm
syntax for pattern aliases
2017-08-18, by Lars Hupel
NEWS: Removed constant subseq; subsumed by strict_mono
2017-08-17, by eberlm
support for incremental update according to session graph structure;
2017-08-17, by wenzelm
Merged
2017-08-17, by eberlm
Replaced subseq with strict_mono
2017-08-17, by eberlm
fix document
2017-08-17, by Lars Hupel
more complete session (amending e77ea0ea7f2c);
2017-08-17, by wenzelm
clarified imports;
2017-08-17, by wenzelm
more complete session (amending 783861a66a60);
2017-08-17, by wenzelm
added lemma
2017-08-17, by nipkow
more reorganization around sorted_wrt
2017-08-16, by nipkow
merged
2017-08-15, by paulson
fixed the previous commit (henstock_lemma)
2017-08-15, by paulson
merged
2017-08-15, by paulson
tidying up henstock_lemma
2017-08-15, by paulson
merged
2017-08-15, by nipkow
NEWS sorted_wrt
2017-08-15, by nipkow
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
2017-08-15, by nipkow
merged
2017-08-15, by wenzelm
Added tag Isabelle2017-RC0 for changeset a5dd01b68218
2017-08-15, by wenzelm
merged
2017-08-15, by paulson
merged
2017-08-15, by paulson
tackling another nightmare proof
2017-08-15, by paulson
extended TSTP type parser + tuned messages
2017-08-15, by blanchet
added debugging function
2017-08-15, by blanchet
merged
2017-08-15, by nipkow
added Min_mset and Max_mset
2017-08-15, by nipkow
NEWS;
2017-08-15, by wenzelm
merged
2017-08-14, by paulson
patching the previous commit
2017-08-14, by paulson
merged
2017-08-14, by paulson
further Hensock tidy-up
2017-08-14, by paulson
separate file for priority queue interface; extended Leftist_Heap.
2017-08-14, by nipkow
tuned GUI;
2017-08-14, by wenzelm
tuned GUI;
2017-08-14, by wenzelm
proper tooltip (amending fd8a65b026f1);
2017-08-14, by wenzelm
updated to scala-2.12.3;
2017-08-14, by wenzelm
auto update;
2017-08-14, by wenzelm
updated to jdk-8u144;
2017-08-14, by wenzelm
tuned GUI;
2017-08-14, by wenzelm
more explicit failure;
2017-08-14, by wenzelm
explicit indication of consolidated nodes;
2017-08-14, by wenzelm
further tidying
2017-08-13, by paulson
general rationalisation of Analysis
2017-08-13, by paulson
merged
2017-08-12, by paulson
cleanup of integral_norm_bound_integral
2017-08-12, by paulson
be more explicit on type dlist
2017-08-12, by haftmann
code generation for Gcd and Lcm when sets are implemented by red-black trees
2017-08-12, by haftmann
merged
2017-08-12, by paulson
more Henstock_Kurzweil_Integration cleanup
2017-08-11, by paulson
merged
2017-08-10, by paulson
even more horrible proofs disentangled
2017-08-10, by paulson
merged
2017-08-11, by Lars Hupel
fmap :: size
2017-08-11, by Lars Hupel
avoid spurious output after exit;
2017-08-11, by wenzelm
updated package version;
2017-08-11, by wenzelm
proper state_panel exit;
2017-08-11, by wenzelm
Some facts about orders of zeros
2017-08-11, by eberlm
Winding numbers for rectangular paths
2017-08-10, by eberlm
misc tuning and modernization;
2017-08-10, by wenzelm
auto update;
2017-08-10, by wenzelm
prefer https for the sake of "npm run vscode:prepublish";
2017-08-10, by wenzelm
tuned;
2017-08-10, by wenzelm
fundamental_theorem_of_calculus_interior: more cleanup
2017-08-09, by paulson
more cleanup of fundamental_theorem_of_calculus_interior
2017-08-09, by paulson
added lemmas
2017-08-09, by nipkow
merged
2017-08-08, by paulson
more cleanup of fundamental_theorem_of_calculus_interior
2017-08-08, by paulson
partly unravelled fundamental_theorem_of_calculus_interior
2017-08-08, by paulson
more unknotting
2017-08-08, by paulson
merged
2017-08-08, by wenzelm
misc tuning and modernization;
2017-08-08, by wenzelm
maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
2017-08-08, by wenzelm
clarified signature;
2017-08-08, by wenzelm
tuned;
2017-08-08, by wenzelm
Merged
2017-08-08, by eberlm
Merged
2017-08-07, by eberlm
Merged
2017-08-04, by eberlm
Removed unnecessary constant 'ball' from Formal_Power_Series
2017-08-03, by eberlm
merged;
2017-08-07, by wenzelm
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
2017-08-07, by wenzelm
more synchronized Execution.snapshot;
2017-08-07, by wenzelm
tuned spelling;
2017-08-07, by wenzelm
tuned;
2017-08-07, by wenzelm
tuned;
2017-08-07, by wenzelm
merged
2017-08-07, by paulson
more Henstock_Kurzweil_Integration cleanup
2017-08-07, by paulson
tuning imports
2017-08-07, by blanchet
use TFF0 with E 2.0 and above
2017-08-07, by blanchet
E 2.0 component
2017-08-07, by blanchet
updated remote Vampire version
2017-08-07, by blanchet
merged
2017-08-06, by paulson
more integration cleanups
2017-08-06, by paulson
slightly generalized card_lists_distinct_length_eq; renamed specialized card_lists_distinct_length_eq to card_lists_distinct_length_eq'; tuned
2017-08-06, by bulwahn
merged
2017-08-06, by paulson
further cleanup of "guess"
2017-08-06, by paulson
towards a cleanup of Henstock_Kurzweil_Integration.thy
2017-08-06, by paulson
merged
2017-08-06, by wenzelm
proper check for active server;
2017-08-06, by wenzelm
clarified signature;
2017-08-06, by wenzelm
tuned signature;
2017-08-06, by wenzelm
handle server connections;
2017-08-06, by wenzelm
clarified database names;
2017-08-06, by wenzelm
more options;
2017-08-06, by wenzelm
support for resident Isabelle servers;
2017-08-05, by wenzelm
default according to Java API, instead of jEdit usage;
2017-08-05, by wenzelm
do not fall back on nbe if plain evaluation fails
2017-08-06, by haftmann
final tidying up of lemma bounded_variation_absolutely_integrable_interval
2017-08-05, by paulson
finally rid of finite_product_dependent
2017-08-05, by paulson
more cleanup
2017-08-05, by paulson
trying to disentangle bounded_variation_absolutely_integrable_interval
2017-08-05, by paulson
merged
2017-08-04, by paulson
more horrible proofs disentangled
2017-08-04, by paulson
tuned
2017-08-04, by haftmann
more structural sharing between common target Generic_Target.init
2017-08-04, by haftmann
exit always refers to the bottom of a nested local theory stack, after_close always to all non-bottom elements
2017-08-04, by haftmann
treat exit separate from regular local theory operations
2017-08-04, by haftmann
provide explicit variant initializers for regular named target vs. almost-named target
2017-08-04, by haftmann
prefer explicit datatype over implicit sum;
2017-08-04, by haftmann
compactified output
2017-08-04, by haftmann
lifting setup for char
2017-08-03, by haftmann
one single plugin for code type declarations avoids problems when bootstrapping new plugins over types which have been both declared concrete and abstract in their code historiy
2017-08-03, by haftmann
uniform namespace handling for both concrete and abstract types, following 32e0da92c786
2017-08-03, by haftmann
clarified
2017-08-03, by haftmann
corrected slip
2017-08-03, by haftmann
tuned
2017-08-03, by haftmann
work around weakness in export calculation when generating OCaml code
2017-08-03, by haftmann
tuned
2017-08-03, by haftmann
pass option recommended by Andy Reynolds to CVC4 1.5 (released) or better
2017-08-03, by blanchet
updated CVC4 component to official 1.5 release
2017-08-03, by blanchet
merged
2017-08-03, by paulson
eliminated more "guess", etc.
2017-08-03, by paulson
merged
2017-08-03, by paulson
more tidying
2017-08-03, by paulson
more tidying up
2017-08-03, by paulson
merged
2017-08-03, by paulson
merged
2017-08-03, by paulson
removed all "guess"
2017-08-02, by paulson
tuned
2017-08-03, by nipkow
merged
2017-08-03, by nipkow
added lemmas
2017-08-03, by nipkow
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
2017-08-02, by haftmann
merged
2017-08-03, by nipkow
generalized lemma
2017-08-02, by nipkow
tuned references
2017-08-01, by haftmann
fixed another horrible proof
2017-08-02, by paulson
misc tuning and modernization;
2017-08-01, by wenzelm
isabelle update_cartouches -c -t;
2017-08-01, by wenzelm
misc tuning and modernization;
2017-08-01, by wenzelm
new lemma
2017-08-01, by nipkow