isabelle: Graph

abandoned attempt to unify sublocale and interpretation into global theories
2015-12-19, by haftmann
updated Cygwin (somewhere after 1.7.35-1);
2015-12-21, by wenzelm
merged
2015-12-21, by wenzelm
merged
2015-12-21, by wenzelm
tuned message;
2015-12-21, by wenzelm
more explicit ML profiling, with official Isabelle output;
2015-12-21, by wenzelm
discontinued built-in profiling: avoid danger of conflicting invocations (multithreading etc.);
2015-12-21, by wenzelm
clarified length of block with pre-existant forced breaks;
2015-12-21, by wenzelm
Probability: fix coercions (real ~> real_of_enat)
2015-12-21, by hoelzl
Transcendental: use [simp]-canonical form - (pi/2)
2015-12-21, by hoelzl
moved some theorems from the CLT proof; reordered some theorems / notation
2015-12-17, by hoelzl
tuned whitespace;
2015-12-20, by wenzelm
tuned signature;
2015-12-20, by wenzelm
renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
2015-12-20, by wenzelm
proper formatting via Pretty.string_of;
2015-12-20, by wenzelm
unused;
2015-12-20, by wenzelm
tuned;
2015-12-20, by wenzelm
prune old document versions more frequently, for reduced heap usage;
2015-12-19, by wenzelm
merged
2015-12-19, by wenzelm
more explicit Pretty.Tree, like in ML;
2015-12-19, by wenzelm
tuned;
2015-12-19, by wenzelm
clarified underlying datatypes;
2015-12-19, by wenzelm
tuned;
2015-12-19, by wenzelm
prefer default focus policy, like Output dockable;
2015-12-19, by wenzelm
tuned;
2015-12-19, by wenzelm
tuned signature;
2015-12-19, by wenzelm
support for blocks with consistent breaks;
2015-12-19, by wenzelm
preserve break indentation;
2015-12-19, by wenzelm
support pretty break indent, like underlying ML systems;
2015-12-17, by wenzelm
register record functions as 'Spec_Rules'
2015-12-19, by blanchet
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
2015-12-19, by blanchet
removed subsumed dependency
2015-12-19, by blanchet
removed dead code
2015-12-19, by blanchet
add serialisation for abs on integer to target language operation
2015-12-18, by Andreas Lochbihler
add gcd instance for integer and serialisation to target language operations
2015-12-18, by Andreas Lochbihler
merged
2015-12-16, by wenzelm
tuned whitespace;
2015-12-16, by wenzelm
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
2015-12-16, by wenzelm
tuned signature -- clarified modules;
2015-12-15, by wenzelm
unused;
2015-12-15, by wenzelm
unused;
2015-12-15, by wenzelm
Merge
2015-12-15, by paulson
New complex analysis material
2015-12-15, by paulson
infix syntax for measurable set
2015-11-25, by hoelzl
more standard term equality;
2015-12-14, by wenzelm
tuned;
2015-12-14, by wenzelm
tuned signature;
2015-12-14, by wenzelm
tuned message;
2015-12-14, by wenzelm
merged
2015-12-13, by wenzelm
more general types Proof.method / context_tactic;
2015-12-13, by wenzelm
tuned;
2015-12-12, by wenzelm
clarified ML scopes;
2015-12-12, by wenzelm
clarified ML scopes;
2015-12-12, by wenzelm
tuned;
2015-12-12, by wenzelm
unused;
2015-12-12, by wenzelm
tuned;
2015-12-12, by wenzelm
clarified modules;
2015-12-11, by wenzelm
modernized
2015-12-12, by haftmann
modernized
2015-12-12, by haftmann
modernized
2015-12-11, by haftmann
isabelle update_cartouches -c -t;
2015-12-10, by wenzelm
proper checksum for cygwin-20151210.tar.gz (some snapshot after 1.7.35-1);
2015-12-10, by wenzelm
avoid application spurious startup error;
2015-12-10, by wenzelm
current Cygwin snapshot in preparation of release;
2015-12-10, by wenzelm
hardwired LANG, to avoid sporadic surprises with local environments;
2015-12-10, by wenzelm
make SML/NJ happy;
2015-12-10, by wenzelm
not_leE -> not_le_imp_less and other tidying
2015-12-10, by paulson
clarified terminology
2015-12-07, by haftmann
tuned;
2015-12-09, by wenzelm
tuned signature;
2015-12-09, by wenzelm
tuned signature;
2015-12-09, by wenzelm
tuned;
2015-12-09, by wenzelm
more direct use of Token.src as token list;
2015-12-09, by wenzelm
merged
2015-12-09, by wenzelm
unused;
2015-12-09, by wenzelm
merged
2015-12-09, by wenzelm
clarified type Token.src: plain token list, with usual implicit value assignment;
2015-12-09, by wenzelm
tuned;
2015-12-09, by wenzelm
tuned;
2015-12-08, by wenzelm
added Proof_Context.add_thms_dynamic, which is potentially useful for Eisbach;
2015-12-08, by wenzelm
sorted out eventually_mono
2015-12-09, by paulson
tightened invariant
2015-12-08, by nipkow
isabelle update_cartouches -c -t;
2015-12-07, by wenzelm
Merge
2015-12-07, by paulson
Cauchy's integral formula for circles. Starting to fix eventually_mono.
2015-12-07, by paulson
Merged
2015-12-07, by eberlm
Generalised derivative rule for division on formal power series
2015-12-07, by eberlm
tuned;
2015-12-07, by wenzelm
more thorough update request: semantic state of command may have changed elsewise;
2015-12-07, by wenzelm
tuned signature;
2015-12-07, by wenzelm
tuned whitespace;
2015-12-07, by wenzelm
isabelle update_cartouches -c -t;
2015-12-07, by wenzelm
isabelle update_cartouches -c -t;
2015-12-07, by wenzelm
tuned;
2015-12-07, by wenzelm
tuned;
2015-12-06, by wenzelm
updated to polyml-5.6-20151206, which presumably improves stability on Windows;
2015-12-06, by wenzelm
discontinued intermediate polyml-5.5.3, assuming the coming release will be polyml-5.6;
2015-12-06, by wenzelm
added AA trees
2015-12-06, by nipkow
tuned
2015-12-06, by nipkow
tuned
2015-12-05, by nipkow
avoid name clashes
2015-12-05, by nipkow
added Brother12_Map
2015-12-05, by nipkow
tuned docs
2015-12-04, by blanchet
more documentation on 'size' plugin
2015-12-04, by blanchet
nicer error when the given size function has the wrong type
2015-12-04, by blanchet
merged
2015-12-04, by nipkow
added 1-2 brother trees
2015-12-04, by nipkow
updated SMT certificates
2015-12-04, by blanchet
removed needless complication for modern SMT solvers
2015-12-04, by blanchet
tuned language
2015-12-03, by haftmann
moved section according to supposed order of interest
2015-12-03, by haftmann
consolidated documentation
2015-12-03, by haftmann
modernized
2015-12-03, by haftmann
tuned sections
2015-12-03, by haftmann
modernized
2015-12-02, by haftmann
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
2015-12-02, by haftmann
prefer conventional read/check distinction over manual check
2015-12-02, by haftmann
clarified role of context for reading rewrite specifications
2015-12-02, by haftmann
formally correct context for export, which got screwed up in 87203a0f0041
2015-12-02, by haftmann
tuned whitespace
2015-12-02, by haftmann
removed needless ML function
2015-12-01, by blanchet
tuned whitespace
2015-12-01, by blanchet
reverted inadvertently qfinished/pushed change r164eeb2ab675
2015-12-01, by blanchet
merged
2015-12-01, by Andreas Lochbihler
add formalisation of Bourbaki-Witt fixpoint theorem
2015-12-01, by Andreas Lochbihler
add lemmas
2015-12-01, by Andreas Lochbihler
strengthen lemma
2015-12-01, by Andreas Lochbihler
Merge
2015-12-01, by paulson
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
2015-12-01, by paulson
set "transfer_rule" attribute more generously
2015-12-01, by blanchet
tuned whitespace
2015-12-01, by blanchet
misc tuning and modernization;
2015-11-30, by wenzelm
misc tuning and modernization;
2015-11-30, by wenzelm
tuned;
2015-11-30, by wenzelm
avoid 'hence' and 'thus' in generated proofs
2015-11-30, by blanchet
removed tracing
2015-11-30, by blanchet
RBT invariants for insert
2015-11-29, by nipkow
removed junk;
2015-11-28, by wenzelm
merged
2015-11-27, by wenzelm
more reactive GUI;
2015-11-27, by wenzelm
tuned;
2015-11-27, by wenzelm
paint root black after insert and delete
2015-11-27, by nipkow
observe option "indent";
2015-11-25, by wenzelm
more scalable GUI;
2015-11-24, by wenzelm
paint gutter text on base line of main text area, to accomodate extra line spacing without special tricks (see also jEdit bug #3717 and its fix in SVN 23977, which does not quite work: odd jumping positions on vertical cursor movement);
2015-11-24, by wenzelm
Ported old example to use (co)datatypes
2015-11-24, by traytel
discontinued Mac OS X 10.7 Lion (macbroy6);
2015-11-23, by wenzelm
merged
2015-11-23, by wenzelm
clarified font: GUI defaults might change dynamically;
2015-11-23, by wenzelm
updated platform baseline to Mac OS X 10.8 Mountain Lion;
2015-11-23, by wenzelm
updated to polyml-5.6-20151123;
2015-11-23, by wenzelm
Merge
2015-11-23, by paulson
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
2015-11-23, by paulson
bundle main sources read-only, to avoid accidental editing of imported theories etc.;
2015-11-23, by wenzelm
more symbols;
2015-11-22, by wenzelm
some GC options that potentially improve reactivity;
2015-11-22, by wenzelm
more thorough completion rendering, e.g. "Un";
2015-11-22, by wenzelm
tuned;
2015-11-22, by wenzelm
Updates to the revision history of the locales tutorial.
2015-11-21, by ballarin
Clarify locale qualifiers: output and tutorial.
2015-11-21, by ballarin
tuned proofs;
2015-11-21, by wenzelm
tuned;
2015-11-21, by wenzelm
double flush to ensure persistent "state" output is reset;
2015-11-21, by wenzelm
reverted 2abbe7d700e9: "state" output is not necessarily proof state;
2015-11-21, by wenzelm
clarified default (again) in accordance to with Output dockable, despite more CPU resources requirements;
2015-11-21, by wenzelm
more thorough update of options;
2015-11-21, by wenzelm
limit statistics, to avoid exhaustion of heap space or GUI time;
2015-11-21, by wenzelm
render snapshot.is_outdated in text overview, where other status information is shown already;
2015-11-21, by wenzelm
avoid flashing of main text area (visual "grey-out") due to spurious edits, e.g. State panel auto-update;
2015-11-21, by wenzelm
clarified default;
2015-11-21, by wenzelm
recovered auto update from f9aaca00be49;
2015-11-21, by wenzelm
less intrusive rendering, notably for State dockable;
2015-11-21, by wenzelm
clarified rendering of Markup.DOC: like Markup.PATH / Markup.URL;
2015-11-21, by wenzelm
more direct access to option "editor_output_state";
2015-11-21, by wenzelm
tuned;
2015-11-21, by wenzelm
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
2015-11-20, by wenzelm
Now just a few seconds faster
2015-11-20, by paulson
merged
2015-11-20, by nipkow
tuned
2015-11-20, by nipkow
Theory of homotopic paths (from HOL Light), plus comments and minor refinements
2015-11-20, by paulson
merged
2015-11-20, by nipkow
tuned
2015-11-20, by nipkow
explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory
2015-11-19, by haftmann
tuned;
2015-11-19, by wenzelm
tuned whitespace;
2015-11-19, by wenzelm
trim lines for @{theory_text} similarly to @{text};
2015-11-19, by wenzelm
tuned;
2015-11-19, by wenzelm
tuned and converted to cmp
2015-11-19, by nipkow
misc. changes to Imperative-HOL from Peter Gammie
2015-11-19, by Lars Hupel
Refine the supression of abbreviations for morphisms that are not identities.
2015-11-18, by ballarin
Merge
2015-11-18, by paulson
New theorems mostly from Peter Gammie
2015-11-18, by paulson
make SML/NJ happy;
2015-11-18, by wenzelm
converted to cmp
2015-11-18, by nipkow
moved lemmas
2015-11-18, by nipkow
derive lemmas uniformly
2015-11-17, by nipkow
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
2015-11-17, by paulson
converted lookup to cmp
2015-11-17, by nipkow
removed lemmas that were only needed for old version of isin.
2015-11-17, by nipkow
clarified contexts by factoring out reading and definition of mixins
2015-11-16, by haftmann
merged
2015-11-16, by Andreas Lochbihler
export internal definition
2015-11-16, by Andreas Lochbihler
corrected inefficient implementation
2015-11-16, by nipkow
more tracing in MaSh
2015-11-16, by blanchet
tuned names
2015-11-16, by nipkow
NEWS
2015-11-16, by nipkow
formally correct context for export
2015-11-15, by haftmann
merged
2015-11-15, by wenzelm
merged
2015-11-15, by wenzelm
option "inductive_defs" controls exposure of def and mono facts;
2015-11-15, by wenzelm
tuned message;
2015-11-14, by wenzelm
added pretty syntax
2015-11-15, by nipkow
tuned white space
2015-11-15, by nipkow
leftover from 27ca6147e3b3
2015-11-15, by haftmann
tuned whitespace
2015-11-15, by haftmann
NEWS
2015-11-15, by haftmann
droppen diagnostic junk from 4b53042d7a40
2015-11-15, by haftmann
represent both algebraic and local-theory views on locale interpretation in interfaces
2015-11-14, by haftmann
tuned -- share implementations as far as appropriate
2015-11-14, by haftmann
prefer "rewrites" and "defines" to note rewrite morphisms
2015-11-14, by haftmann
coalesce permanent_interpretation.ML with interpretation.ML
2015-11-14, by haftmann
separate ML module for interpretation
2015-11-14, by haftmann
reverted half-baken 7d1127ac2251
2015-11-14, by haftmann
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
2015-11-14, by haftmann