isabelle: Graph

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
tuned signature
2016-08-23, by traytel
replaced the confusing int parameter by bool
2016-08-19, by nipkow
remove spurious find_theorems
2016-08-18, by hoelzl
HOL-Probability: Projective_Limit was missing (cf. 44ce6b524ff3); tuned
2016-08-18, by hoelzl
removed debug output
2016-08-18, by traytel
derive pred_mono property for BNFs
2016-08-18, by traytel
Tuned L'Hospital
2016-08-17, by eberlm
merged
2016-08-17, by boehmes
more complete simpset for linear arithmetic to avoid warnings: terms such as (2x + 2y)/2 can then be simplified by the linear arithmetic prover during its proof replay
2016-08-17, by boehmes
merged
2016-08-17, by traytel
coinduction method accepts a list of coinduction rules (takes the first matching one)
2016-03-04, by traytel
more robust;
2016-08-16, by wenzelm
clarified presentation order, according to typical amounts;
2016-08-16, by wenzelm
present ML timing as well;
2016-08-16, by wenzelm
Polynomial algebra cleanup (tuned)
2016-08-16, by eberlm
Polynomial algebra cleanup
2016-08-16, by eberlm
provide index.html;
2016-08-14, by wenzelm
cpu time is optional (see Timing.message_resources);
2016-08-14, by wenzelm
proper display of "_";
2016-08-14, by wenzelm
clarified options and arguments;
2016-08-14, by wenzelm
updated NEWS
2016-08-14, by blanchet
optimized parent computation in MaSh
2016-08-14, by blanchet
avoid loading MaSh file first time around for higher responsiveness of Sledgehammer
2016-08-14, by blanchet
tuned MaSh's metacharacters to avoid needless decoding
2016-08-14, by blanchet
optimization in MaSh parsing
2016-08-14, by blanchet
tuned ML
2016-08-14, by blanchet
removed trailing final stops in Nitpick messages
2016-08-14, by blanchet
killed final stops in Sledgehammer and friends
2016-08-14, by blanchet
tuned message
2016-08-14, by blanchet
tuning punctuation in messages output by Isabelle
2016-08-14, by blanchet
tuning whitespace in output syntax
2016-08-14, by blanchet
gnuplot presentation similar to former isatest-statistics;
2016-08-13, by wenzelm
tuned;
2016-08-13, by wenzelm
statistics from session build output;
2016-08-13, by wenzelm
more uniform output;
2016-08-13, by wenzelm
added [simp] lemmas
2016-08-13, by nipkow
more robust HTML rendering of hidden control symbols: Vacuous font bypasses minimal font-size restrictions of common browsers, transparent colour imitates hidden visibility while copy-paste still works;
2016-08-12, by wenzelm
merged
2016-08-12, by wenzelm
active jEdit actions;
2016-08-12, by wenzelm
more symbols;
2016-08-12, by wenzelm
clarified syntax;
2016-08-12, by wenzelm
updated;
2016-08-12, by wenzelm
some icons from Symbola font;
2016-08-12, by wenzelm
more latex symbols, notably for embedded ML;
2016-08-12, by wenzelm
uniform ML and document antiquotations;
2016-08-12, by wenzelm
proper completion of path cartouche (amending 5a7c919a4ada);
2016-08-12, by wenzelm
clarified error;
2016-08-12, by wenzelm
more uniform path syntax (like url);
2016-08-12, by wenzelm
liberal name as in document antiquotations;
2016-08-12, by wenzelm
tuned;
2016-08-12, by wenzelm
clarified antiquotations;
2016-08-11, by wenzelm
tuned error;
2016-08-11, by wenzelm
tuned whitespace;
2016-08-11, by wenzelm
suppress ASCII art;
2016-08-11, by wenzelm
added lemma
2016-08-12, by nipkow
tuned
2016-08-12, by nipkow
Extracted floorlog and bitlen to separate theory Log_Nat
2016-08-12, by nipkow
lists form a monoid
2016-08-10, by haftmann
formal passive interpretation proofs for conj and disj
2016-08-10, by haftmann
add monotonicity propertyies of `mult1` and `mult`
2016-08-08, by Bertram Felgenhauer
keeping lifting rules local
2016-08-10, by haftmann
epheremal interpretation keeps auxiliary definition localized
2016-08-10, by haftmann
tuned order of declarations and proofs
2016-08-10, by haftmann
tuned
2016-08-11, by nipkow
simplified theory hierarchy;
2016-08-10, by wenzelm
misc tuning and modernization;
2016-08-10, by wenzelm
misc tuning and modernization;
2016-08-10, by wenzelm
misc tuning and modernization;
2016-08-10, by wenzelm
merged
2016-08-10, by nipkow
"split add" -> "split".
2016-08-10, by nipkow
tuned proofs;
2016-08-10, by wenzelm
"split add" -> "split"
2016-08-10, by nipkow
merged
2016-08-09, by wenzelm
API for Isabelle Jenkins continuous integration services;
2016-08-09, by wenzelm
more operations;
2016-08-09, by wenzelm
support for JSON parsing;
2016-08-09, by wenzelm
New theory Balance_List
2016-08-09, by nipkow
more operations;
2016-08-09, by wenzelm
merged;
2016-08-09, by wenzelm
print name in parsable form;
2016-08-09, by wenzelm
clarified bootstrap;
2016-08-09, by wenzelm
merged
2016-08-09, by nipkow
adapted ZF,FOL,CCL,LCF to modified splitter
2016-08-09, by nipkow
introduced aggressive splitter "split!"
2016-08-09, by nipkow
Tuned primes
2016-08-09, by eberlm
Merged
2016-08-09, by eberlm
is_prime -> prime
2016-08-08, by eberlm
Item_Net.retrieve_matching requires beta-eta normal form (amending 8976c5bc9e97);
2016-08-08, by wenzelm
merged
2016-08-08, by wenzelm
tuned proof;
2016-08-08, by wenzelm
tuned;
2016-08-08, by wenzelm
tuned;
2016-08-08, by wenzelm
rename HOL-Multivariate_Analysis to HOL-Analysis.
2016-08-08, by hoelzl
move measure theory from HOL-Probability to HOL-Multivariate_Analysis
2016-08-05, by hoelzl
misc tuning and modernization;
2016-08-07, by wenzelm
more informative 'prf' and 'full_prf', based on HOL/Proofs/ex/XML_Data.thy;
2016-08-06, by wenzelm
tuned signature;
2016-08-06, by wenzelm
some additions to FSet
2016-08-06, by Lars Hupel
tuned
2016-08-06, by nipkow
clarified Sidekick setup;
2016-08-05, by wenzelm
more tight filtering;
2016-08-05, by wenzelm
tuned;
2016-08-05, by wenzelm
clarified -- more standard maxidx;
2016-08-05, by wenzelm
tuned -- maxidx unused;
2016-08-05, by wenzelm
tuned;
2016-08-05, by wenzelm
tuned;
2016-08-05, by wenzelm
merged
2016-08-05, by wenzelm
misc tuning and modernization;
2016-08-05, by wenzelm
tuned whitespace;
2016-08-05, by wenzelm
Sidekick parser for isabelle-ml and sml mode;
2016-08-05, by wenzelm
prefer hardwired "nothing";
2016-08-04, by wenzelm
NEWS;
2016-08-04, by wenzelm
clarified handling of plain theory commands;
2016-08-04, by wenzelm
support for context block structure in Sidekick;
2016-08-04, by wenzelm
tuned;
2016-08-04, by wenzelm
clarified modules;
2016-08-04, by wenzelm
clarified modules;
2016-08-04, by wenzelm
merged
2016-08-05, by nipkow
added missing lemmas
2016-08-05, by nipkow
fixed floor proof
2016-08-05, by nipkow
fixed floor proofs
2016-08-05, by nipkow
added min_height
2016-08-05, by nipkow
tuned floor lemmas
2016-08-05, by nipkow
more lemmas
2016-08-05, by nipkow
clean up prove for inter_interior_unions_intervals
2016-08-05, by hoelzl
HOL-Multivariate_Analysis: rename theories for more descriptive names
2016-08-04, by hoelzl
HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
2016-08-04, by hoelzl
include 'begin' and 'end' structure in text folds;
2016-08-03, by wenzelm
tuned proof;
2016-08-02, by wenzelm
proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
2016-08-02, by wenzelm
more symbols;
2016-08-02, by wenzelm
misc tuning and modernization;
2016-08-02, by wenzelm
implicit keyword completion only for actual words (amending 73939a9b70a3);
2016-08-02, by wenzelm
merged
2016-08-02, by wenzelm
tuned;
2016-08-02, by wenzelm
tuned signature -- prover-independence is presently theoretical;
2016-08-02, by wenzelm
tuned;
2016-08-02, by wenzelm
avoid confusion with 'case' and "cases";
2016-08-02, by wenzelm
tuned;
2016-08-02, by wenzelm
clarified: 'imports' is de-facto mandatory;
2016-08-02, by wenzelm
support 'abbrevs' within theory header;
2016-08-02, by wenzelm
tuned;
2016-08-02, by wenzelm
more natural definition of type finmap
2016-08-02, by immler
tuned proof;
2016-08-01, by wenzelm
misc tuning and modernization;
2016-08-01, by wenzelm
uniform server startup like windows and macos, for improved robustness if jEdit is terminated abruptly;
2016-08-01, by wenzelm
more restrictive retrieval of rules for matching instead of unification -- relevant for performance of printing terms;
2016-08-01, by wenzelm
misc tuning and modernization;
2016-07-31, by wenzelm
clarified imports;
2016-07-31, by wenzelm
simplified theory structure;
2016-07-31, by wenzelm
misc tuning and modernization;
2016-07-31, by wenzelm
tuned;
2016-07-30, by wenzelm
merged
2016-07-29, by wenzelm
more accurate cong del;
2016-07-29, by wenzelm
made generation of transfer goals more robust w.r.t. dead variables
2016-07-29, by traytel
merged
2016-07-29, by Andreas Lochbihler
prefer [simp] over [iff] as [iff] break HOL-UNITY
2016-07-29, by Andreas Lochbihler
fix LaTeX error
2016-07-29, by Andreas Lochbihler
add lemmas contributed by Peter Gammie
2016-07-29, by Andreas Lochbihler
more instantiations for multiset
2016-07-29, by fleury
merged
2016-07-28, by wenzelm
misc tuning and modernization;
2016-07-28, by wenzelm
updated to jdk-8u102;
2016-07-27, by wenzelm
numerical bounds on pi
2016-07-28, by immler
more on type class hierarchy
2016-07-24, by haftmann
simplified
2016-07-24, by haftmann
text antiquotation for locales (similar to classes)
2016-07-24, by haftmann
NEWS: Primes
2016-07-27, by Manuel Eberl
honor sorts in (co)datatype declarations
2016-07-26, by traytel
misc tuning and modernization;
2016-07-26, by wenzelm
more symbols;
2016-07-25, by wenzelm
unused (see 1e9e68247ad1);
2016-07-25, by wenzelm
merged
2016-07-25, by wenzelm
misc tuning and modernization;
2016-07-22, by wenzelm
misc tuning and modernization;
2016-07-22, by wenzelm
clarified def vs. ref focus, e.g. for calculation vs. command refs;
2016-07-22, by wenzelm
entity markup for calculation;
2016-07-22, by wenzelm
tuned;
2016-07-22, by wenzelm
more markup for unstructured calculation;
2016-07-22, by wenzelm
tuned proofs -- avoid unstructured calculation;
2016-07-22, by wenzelm
tuned proofs -- avoid improper use of "this";
2016-07-22, by wenzelm
added new vcg based on existentially quantified while-rule
2016-07-23, by nipkow
Removed redundant material related to primes
2016-07-22, by eberlm
Merged
2016-07-22, by eberlm
Tuned primes
2016-07-22, by eberlm
Overhaul of prime/multiplicity/prime_factors
2016-07-21, by eberlm
merged
2016-07-21, by wenzelm
provide Pure.simp/simp_all, which only know about meta-equality;
2016-07-20, by wenzelm
clarified imports;
2016-07-20, by wenzelm
tuned;
2016-07-20, by wenzelm
oops;
2016-07-20, by wenzelm
completion templates for commands involving "begin ... end" blocks;
2016-07-20, by wenzelm
moved method "use" to Pure;
2016-07-20, by wenzelm
unused (see also 651ea265d568);
2016-07-20, by wenzelm
more instantiations for multiset
2016-07-20, by fleury
adding mset_map to the simp rules
2016-07-20, by fleury
misc tuning and simplification;
2016-07-19, by wenzelm
misc tuning and simplification;
2016-07-19, by wenzelm
added missing transfer rule
2016-07-19, by Lars Hupel
Linux platform base-line is Ubuntu 12.04 LTS;
2016-07-19, by wenzelm
more precise error information for dynamic Scala tools
2016-07-17, by Lars Hupel
tuned signature;
2016-07-16, by wenzelm