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.
eliminated old defs;
2016-01-11, by wenzelm
Deleted problematic code equation in Binomial temporarily.
2016-01-12, by eberlm
add reference
2016-01-12, by Andreas Lochbihler
merged
2016-01-12, by Andreas Lochbihler
add BNF instance for Dlist
2016-01-12, by Andreas Lochbihler
crediting LCP in CONTRIBUTORS
2016-01-12, by paulson
more careful witness' type analysis
2016-01-12, by traytel
removed outdated example
2016-01-12, by traytel
remove unused code
2016-01-12, by matichuk
remove Eisbach's dependency on HOL
2016-01-12, by matichuk
match method now makes proper use of context_tactic
2016-01-11, by matichuk
merged
2016-01-11, by paulson
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
2016-01-11, by paulson
added AA_Map; tuned titles
2016-01-11, by nipkow
tuned
2016-01-11, by nipkow
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
2016-01-11, by eberlm
generalized proofs
2016-01-11, by immler
avoid generating TFF1 or polymorphic DFG constructs in Vampire or SPASS problems for goals containing schematic type variables
2016-01-11, by blanchet
tuning
2016-01-11, by blanchet
exported ML function
2016-01-11, by blanchet
setup code generation for filters as suggested by Florian
2016-01-11, by hoelzl
merged
2016-01-11, by Lars Hupel
filter non-matching prems rather than fail in proof procedure in rare cases; include derived example motivating change and some similar other ones
2016-01-10, by Lukas Bulwahn
isar-ref entry for print_record
2016-01-10, by kleing
add more frequently-run test for print_record
2016-01-10, by kleing
print_record NEWS and CONTRIBUTORS
2016-01-10, by kleing
print_record: diagnostic printing of record definitions
2016-01-10, by kleing
misc tuning and modernization;
2016-01-11, by wenzelm
prune old versions more often, to reduce overall heap requirements;
2016-01-10, by wenzelm
generate HTML version of NEWS, with proper symbol rendering;
2016-01-09, by wenzelm
tuned -- according to ML version;
2016-01-09, by wenzelm
suppress somewhat pointless description (NB: this is displayed in 'print_methods');
2016-01-09, by wenzelm
merged
2016-01-09, by wenzelm
tuned syntax;
2016-01-09, by wenzelm
tuned;
2016-01-09, by wenzelm
\<struct> loses its rendering and is superseded by \<diamondop>;
2016-01-09, by wenzelm
discontinued \<struct> syntax;
2016-01-09, by wenzelm
tuned whitespace;
2016-01-08, by wenzelm
tuned;
2016-01-08, by wenzelm
clarified symbol insertion, depending on buffer encoding;
2016-01-08, by wenzelm
tuned;
2016-01-08, by wenzelm
fix code generation for uniformity: uniformity is a non-computable pure data.
2016-01-08, by hoelzl
add uniform spaces
2016-01-08, by hoelzl
merged
2016-01-08, by wenzelm
merged
2016-01-08, by wenzelm
tuned;
2016-01-08, by wenzelm
merged
2016-01-08, by wenzelm
more uniform treatment of symblinks: avoid confusion when unpacking .tar.gz bundle with NTFS links;
2016-01-07, by wenzelm
tuned signature;
2016-01-07, by wenzelm
prefer non-ASCII output;
2016-01-07, by wenzelm
more uniform treatment of package internals;
2016-01-07, by wenzelm
more thorough GUI update;
2016-01-07, by wenzelm
tuned;
2016-01-07, by wenzelm
added lemma
2016-01-08, by nipkow
Tuned constant approximations
2016-01-08, by eberlm
merged
2016-01-07, by paulson
revisions to limits and derivatives, plus new lemmas
2016-01-07, by paulson
Added formal power series updates to NEWS/CONTRIBUTORS
2016-01-07, by Manuel Eberl
Tuned approximations in Multivariate_Analysis
2016-01-07, by Manuel Eberl
misc tuning for release;
2016-01-06, by wenzelm
add the proof of the central limit theorem
2016-01-06, by hoelzl
nicer 'Spec_Rules' for size function
2016-01-06, by blanchet
updated docs
2016-01-06, by blanchet
updated NEWS
2016-01-06, by blanchet
more complete setup for 'Rat' in Nitpick
2016-01-06, by blanchet
more systematic treatment of dynamic facts, when forming closure;
2016-01-06, by wenzelm
clarified ROOT files;
2016-01-06, by wenzelm
proper Pattern.match and corresponding Envir.subst_term, instead of Envir.norm_term of unify-family;
2016-01-06, by wenzelm
added ML antiquotation @{method};
2016-01-06, by wenzelm
tuned;
2016-01-05, by wenzelm
tuned;
2016-01-05, by wenzelm
isabelle update_cartouches -c -t;
2016-01-05, by wenzelm
merged
2016-01-05, by wenzelm
more realistic Eisbach method invocation from ML;
2016-01-05, by wenzelm
unused;
2016-01-05, by wenzelm
more robust event propagation;
2016-01-05, by wenzelm
Fixed sectioning in HOL/Library/Polynomial
2016-01-05, by eberlm
Merged
2016-01-05, by eberlm
Added some facts about polynomials
2016-01-05, by eberlm
misc tuning for release;
2016-01-05, by wenzelm
merged
2016-01-05, by wenzelm
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
2016-01-05, by wenzelm
tuned;
2016-01-05, by wenzelm
Added summability/Gamma/etc. to NEWS and CONTRIBUTORS
2016-01-05, by eberlm
proper latex setup;
2016-01-05, by wenzelm
updated headers;
2016-01-05, by wenzelm
merged
2016-01-05, by wenzelm
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
2016-01-05, by wenzelm
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
2016-01-05, by hoelzl
merged
2016-01-04, by wenzelm
tuned proofs;
2016-01-04, by wenzelm
node_status update is back on GUI thread (reverting 3ad2b2055ffc) -- avoid potential deadlock of GUI_Thread.now during shutdown, when GUI thread is already terminated;
2016-01-04, by wenzelm
stop dummy sessions as well;
2016-01-04, by wenzelm
clarified order of shutdown;
2016-01-04, by wenzelm
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
2016-01-04, by eberlm
retain ASCII syntax for output, when HOL/Library/Lattice_Syntax is not present (amending e96292f32c3c);
2016-01-03, by wenzelm
proper treatment of RAW bootstrap session;
2016-01-03, by wenzelm
tuned whitespace;
2016-01-03, by wenzelm
more symbols;
2016-01-02, by wenzelm
tuned spacing of \<partial>;
2016-01-02, by wenzelm
eliminated somewhat pointless and obscure options;
2016-01-02, by wenzelm
isabelle update_cartouches -c -t;
2016-01-02, by wenzelm
tuned;
2016-01-02, by wenzelm
proper platform_path for Windows;
2016-01-02, by wenzelm
clarified isabelle jedit command-line;
2016-01-02, by wenzelm
tuned;
2016-01-02, by wenzelm
avoid downloading contrib again;
2016-01-02, by wenzelm
provide server name uniformly on all platforms;
2016-01-02, by wenzelm
more symbols;
2016-01-02, by wenzelm
NEWS;
2016-01-02, by wenzelm
keep platform bundle for reference, e.g. for headless installation;
2016-01-01, by wenzelm
keep generic archive for all platforms -- required for Admin/Release/build_library;
2016-01-01, by wenzelm
oops;
2016-01-01, by wenzelm
Added tag Isabelle2016-RC0 for changeset e18444532fce
2016-01-01, by wenzelm
tuned;
2016-01-01, by wenzelm
updated for release;
2016-01-01, by wenzelm
tuned;
2016-01-01, by wenzelm
more symbols;
2016-01-01, by wenzelm
clarified abbrev;
2016-01-01, by wenzelm
clarified meaning of \<^bold> action, depending on group;
2016-01-01, by wenzelm
clarified groups, notably for Symbols dockable;
2016-01-01, by wenzelm
glyphs for \<bind>, \<then>;
2016-01-01, by wenzelm
tuned order for isar-ref;
2016-01-01, by wenzelm
isabelle update_cartouches -c -t;
2016-01-01, by wenzelm
updated for release;
2015-12-31, by wenzelm
updated to SML/NJ 110.79;
2015-12-31, by wenzelm
misc tuning for release;
2015-12-31, by wenzelm
misc updates for release;
2015-12-31, by wenzelm
expand hard tabs;
2015-12-31, by wenzelm
documentation for "isabelle jedit_client";
2015-12-31, by wenzelm
discontinued documentation of old browser;
2015-12-31, by wenzelm
more precise context -- potentially relevant for Eisbach dummy thm;
2015-12-31, by wenzelm
tuned;
2015-12-31, by wenzelm
updated sumatra_pdf;
2015-12-31, by wenzelm
clarified imports;
2015-12-31, by wenzelm
clarified directory structure;
2015-12-31, by wenzelm
updated isabelle_fonts;
2015-12-31, by wenzelm
proper diamond from lasy10;
2015-12-31, by wenzelm
modernized defs;
2015-12-31, by wenzelm
more symbols;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
isabelle update_cartouches -c -t;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
clarified print modes;
2015-12-30, by wenzelm
updated print modes;
2015-12-30, by wenzelm
modernized Isabelle document markup;
2015-12-30, by wenzelm
clarified print modes: Isabelle symbols are used by default, but "latex" mode needs to be for some syntax forms;
2015-12-30, by wenzelm
clarified print modes;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
removed junk;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
clarified print modes;
2015-12-30, by wenzelm
clarified print modes;
2015-12-30, by wenzelm
clarified print modes;
2015-12-30, by wenzelm
isabelle update_cartouches -c -t;
2015-12-30, by wenzelm
clarified print modes;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
clarified syntax;
2015-12-30, by wenzelm
clarified print modes;
2015-12-30, by wenzelm
proper latex setup;
2015-12-30, by wenzelm
proper latex setup;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
isabelle update_cartouches -c -t;
2015-12-30, by wenzelm
tuned java options;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
simplified abbrevs: exploit ambiguity;
2015-12-29, by wenzelm
more symbols;
2015-12-29, by wenzelm
more symbols;
2015-12-29, by wenzelm
more symbols;
2015-12-29, by wenzelm
avoid immediate completion as ASCII versions that are still used;
2015-12-29, by wenzelm
tuned order for isar-ref manual;
2015-12-29, by wenzelm
more symbols;
2015-12-29, by wenzelm
updated isabelle_fonts;
2015-12-29, by wenzelm
more arrow symbols;
2015-12-29, by wenzelm
more arrow symbols;
2015-12-29, by wenzelm
eliminated obscure macro that is in conflict with amsmath.sty;
2015-12-29, by wenzelm
more abbrevs;
2015-12-29, by wenzelm
support additional abbrevs;
2015-12-29, by wenzelm
tuned;
2015-12-29, by wenzelm
isabelle console: print mode "ASCII";
2015-12-29, by wenzelm
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-29, by wenzelm
more symbols;
2015-12-28, by wenzelm
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-28, by wenzelm
more symbols;
2015-12-28, by wenzelm
use symbols by default;
2015-12-28, by wenzelm
prefer symbols for "Union", "Inter";
2015-12-28, by wenzelm
clarified position information;
2015-12-28, by wenzelm
suppress irrelevant position reports;
2015-12-28, by wenzelm
suppress irrelevant position reports;
2015-12-28, by wenzelm
tuned;
2015-12-28, by wenzelm
more position information;
2015-12-28, by wenzelm
put example into separate session, to restrict precious session image to library theories
2015-12-27, by haftmann
more symbols;
2015-12-28, by wenzelm
prefer symbols for "abs";
2015-12-28, by wenzelm
discontinued ASCII replacement syntax <*>;
2015-12-27, by wenzelm
prefer symbols for "floor", "ceiling";
2015-12-27, by wenzelm
discontinued ASCII replacement syntax <->;
2015-12-27, by wenzelm
more symbols;
2015-12-27, by wenzelm
tuned document;
2015-12-27, by wenzelm
more proofs;
2015-12-27, by wenzelm
tuned;
2015-12-27, by wenzelm
more notation;
2015-12-26, by wenzelm
clarified sessions;
2015-12-26, by wenzelm
tuned;
2015-12-26, by wenzelm
isabelle update_cartouches -c -t;
2015-12-26, by wenzelm
misc tuning and modernization;
2015-12-26, by wenzelm
more proofs, more text;
2015-12-26, by wenzelm
modernized example;
2015-12-26, by wenzelm
tuned proofs and augmented lemmas
2015-12-24, by haftmann
tuned proof
2015-12-24, by haftmann
less ambitious test;
2015-12-23, by wenzelm
tuned;
2015-12-23, by wenzelm
clarified directory structure;
2015-12-23, by wenzelm
updated polyml;
2015-12-23, by wenzelm
clarified context policy to allow multiple dummies;
2015-12-23, by wenzelm
NEWS;
2015-12-23, by wenzelm
tuned;
2015-12-23, by wenzelm
merged
2015-12-23, by wenzelm
tuned module arrangement;
2015-12-23, by wenzelm
tuned module arrangement;
2015-12-23, by wenzelm
check and report source at most once, notably in body of "match" method;
2015-12-23, by wenzelm
transfer rule for bounded_linear of blinfun
2015-12-23, by immler
theory for type of bounded linear functions; differentiation under the integral sign
2015-12-22, by immler
stripped some legacy
2015-12-22, by haftmann
tuned proofs and augmented some lemmas
2015-12-22, by haftmann
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
2015-12-22, by wenzelm
proper full name within the name space of the method definition;
2015-12-22, by wenzelm
tuned signature;
2015-12-22, by wenzelm
isabelle update_cartouches -c -t;
2015-12-22, by wenzelm
Merge
2015-12-22, by paulson
Liouville theorem, Fundamental Theorem of Algebra, etc.
2015-12-22, by paulson
Weierstrass: whitespace
2015-12-22, by hoelzl
merged
2015-12-22, by wenzelm
more thorough event propagation;
2015-12-22, by wenzelm
tuned -- with subtle change of order of evaluation;
2015-12-22, by wenzelm
more accurate lookup of dynamic facts;
2015-12-22, by wenzelm
tuned;
2015-12-22, by wenzelm
tuned;
2015-12-22, by wenzelm
tuned signature;
2015-12-22, by wenzelm
tuned;
2015-12-22, by wenzelm
Bochner integral: prove dominated convergence at_top
2015-12-21, by hoelzl
dead code;
2015-12-21, by wenzelm
tuned spelling;
2015-12-21, by wenzelm
merged
2015-12-21, by wenzelm
misc tuning and modernization;
2015-12-21, by wenzelm
merged
2015-12-21, by haftmann
documentation on last state of the art concerning interpretation
2015-12-19, by haftmann
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
more standard ML, to make SML/NJ more happy;
2015-11-14, by wenzelm
tuned;
2015-11-13, by wenzelm
tuned whitespace;
2015-11-13, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
tip