Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+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.
tuned;
2015-11-13, by wenzelm
tuned whitespace;
2015-11-13, by wenzelm
merged
2015-11-13, by wenzelm
added antiquotation @{doc}, e.g. useful for demonstration purposes;
2015-11-13, by wenzelm
preserve names of for-fixes for faithfully;
2015-11-13, by wenzelm
more documentation;
2015-11-13, by wenzelm
tuned whitespace;
2015-11-13, by wenzelm
more uniform jEdit properties;
2015-11-13, by wenzelm
avoid vacuous quantification, as usual for shared variable scope;
2015-11-13, by wenzelm
support for structure statements in 'assume', 'presume';
2015-11-13, by wenzelm
support short form for \<^theory_text>;
2015-11-12, by wenzelm
MIR decision procedure again working
2015-11-13, by paulson
unnecessary precondition
2015-11-13, by nipkow
Merge
2015-11-13, by paulson
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-13, by paulson
tuned name
2015-11-13, by nipkow
tuned
2015-11-13, by nipkow
use cartouches instead of backquotes
2015-11-12, by blanchet
translation for conjunctive premises
2015-11-12, by nipkow
tuned
2015-11-12, by nipkow
added proof state output warning
2015-11-12, by nipkow
tuned
2015-11-11, by nipkow
merged
2015-11-11, by nipkow
no CRLF
2015-11-11, by nipkow
new conversion theorems for int, nat to float
2015-11-11, by paulson
merged
2015-11-11, by nipkow
uniform proof of lemmas
2015-11-11, by nipkow
merged
2015-11-11, by Andreas Lochbihler
adapt to 90f54d9e63f2
2015-11-11, by Andreas Lochbihler
add various lemmas
2015-11-11, by Andreas Lochbihler
add lemmas
2015-11-11, by Andreas Lochbihler
generalise lemma
2015-11-11, by Andreas Lochbihler
add lemmas for extended nats and reals
2015-11-11, by Andreas Lochbihler
add various lemmas
2015-11-11, by Andreas Lochbihler
cancel complementary terms as arguments to sup/inf in boolean algebras
2015-11-11, by Andreas Lochbihler
add lemmas about monoids and groups
2015-11-11, by Andreas Lochbihler
tuned
2015-11-11, by nipkow
recovered from a9c0572109af;
2015-11-10, by wenzelm
merged
2015-11-10, by wenzelm
tuned whitespace;
2015-11-10, by wenzelm
added @{command}, @{method}, @{attribute};
2015-11-10, by wenzelm
smart quoting of non-identifiers, e.g. jEdit actions;
2015-11-10, by wenzelm
more thorough check_action, including completion;
2015-11-10, by wenzelm
tuned signature;
2015-11-10, by wenzelm
clarified modules;
2015-11-10, by wenzelm
more thorough check_command, including completion;
2015-11-10, by wenzelm
clarified modules;
2015-11-10, by wenzelm
unused;
2015-11-10, by wenzelm
ignore pointless/unused options;
2015-11-10, by wenzelm
added document antiquotation @{theory_text};
2015-11-10, by wenzelm
allow open symboloid;
2015-11-10, by wenzelm
generalized so that is also works for veriT proofs
2015-11-10, by fleury
fixing premises in veriT proof reconstruction
2015-11-10, by fleury
Merge
2015-11-10, by paulson
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-11-10, by paulson
subdegree/shift/cutoff and Euclidean ring instance for formal power series
2015-11-10, by eberlm
prefer static Font -- evade spontaneous change of TextField.font seen with Metal L&F in Plugin Options / Isabelle / General / Apply;
2015-11-09, by wenzelm
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
2015-11-09, by wenzelm
qualifier is mandatory by default;
2015-11-09, by wenzelm
prefer explicit State panel;
2015-11-09, by wenzelm
suppress already persistent state output as well;
2015-11-09, by wenzelm
added option timeout_scale;
2015-11-08, by wenzelm
syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML;
2015-11-07, by wenzelm
clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
2015-11-07, by wenzelm
tuned;
2015-11-07, by wenzelm
less confusing markup;
2015-11-07, by wenzelm
added @{undefined} with somewhat undefined symbol;
2015-11-07, by wenzelm
ML cartouches via control antiquotation;
2015-11-07, by wenzelm
more formal treatment of control symbols;
2015-11-06, by wenzelm
more antiquotations;
2015-11-06, by wenzelm
more antiquotations;
2015-11-06, by wenzelm
retain traditional rendering of \<paragraph>;
2015-11-06, by wenzelm
added glyphs 0x204b, 0x2b1a from DejaVuSansMono;
2015-11-06, by wenzelm
tuned;
2015-11-06, by wenzelm
tuned
2015-11-06, by nipkow
tuned
2015-11-05, by nipkow
updating options to verit
2015-11-05, by fleury
isabelle update_cartouches -c -t;
2015-11-05, by wenzelm
isabelle update_cartouches -c -t;
2015-11-05, by wenzelm
IsabelleText for unusual symbol;
2015-11-05, by wenzelm
isabelle update_cartouches -c;
2015-11-05, by wenzelm
merged
2015-11-05, by nipkow
Convertd to 3-way comparisons
2015-11-05, by nipkow
isabelle update_cartouches -c;
2015-11-05, by wenzelm
symbolic syntax "\<comment> text";
2015-11-05, by wenzelm
avoid ligatures;
2015-11-04, by wenzelm
added propertional dashes from DejaVuSans (not Mono): 0x2013, 0x2014, 0x2015;
2015-11-04, by wenzelm
tuned whitespace;
2015-11-04, by wenzelm
tuned whitespace;
2015-11-04, by wenzelm
tuned whitespace;
2015-11-04, by wenzelm
updated;
2015-11-04, by wenzelm
more antiquotations;
2015-11-04, by wenzelm
document antiquotation @{footnote};
2015-11-04, by wenzelm
dummy input handler to imitate former read-only mode, which has changed its meaning in jedit-5.3.0 as mere hint for saving;
2015-11-04, by wenzelm
eliminated Nitpick's pedantic support for 'emdash'
2015-11-04, by blanchet
tuned;
2015-11-04, by wenzelm
NEWS;
2015-11-04, by wenzelm
Keyword 'rewrites' identifies rewrite morphisms.
2015-11-04, by ballarin
Qualifiers in locale expressions default to mandatory regardless of the command.
2015-11-04, by ballarin
merged
2015-11-03, by wenzelm
tuned signature;
2015-11-03, by wenzelm
prefer Isabelle/Scala Future;
2015-11-03, by wenzelm
prefer Isabelle/Scala Future;
2015-11-03, by wenzelm
tuned imports;
2015-11-03, by wenzelm
more direct task future implementation, with proper cancel operation;
2015-11-03, by wenzelm
tuned;
2015-11-03, by wenzelm
prefer ad-hoc non-worker threads;
2015-11-03, by wenzelm
clarified modules;
2015-11-03, by wenzelm
cancel already running request;
2015-11-03, by wenzelm
added acknowledgement in Binomial.thy
2015-11-03, by eberlm
Merged
2015-11-03, by eberlm
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
2015-11-02, by eberlm
don't pollute local theory with needless names
2015-11-02, by blanchet
allow selectors and discriminators with same name as type
2015-11-02, by blanchet
make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
2015-11-02, by blanchet
merged
2015-11-02, by wenzelm
avoid premature flushing and thus flashing of text area;
2015-11-02, by wenzelm
tuned whitespace;
2015-11-02, by wenzelm
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
2015-11-02, by wenzelm
redundant;
2015-11-02, by wenzelm
tuned whitespace;
2015-11-02, by wenzelm
tuned document;
2015-11-02, by wenzelm
tuned document;
2015-11-02, by wenzelm
tuned document;
2015-11-02, by wenzelm
isabelle update_cartouches -t;
2015-11-02, by wenzelm
avoid highlighted area getting "stuck" after edit;
2015-11-02, by wenzelm
clarified completion of Isabelle symbols within document source;
2015-11-02, by wenzelm
more accurate imports: allow re-uses of base names in PIDE interaction (amending 60c159d490a2);
2015-11-02, by wenzelm
merged
2015-11-02, by nipkow
tuned names and optimized comparison order
2015-11-02, by nipkow
updated CVC4 component to deal with paths with whitespace
2015-11-02, by blanchet
Merged
2015-11-02, by eberlm
Rounding function, uniform limits, cotangent, binomial identities
2015-11-02, by eberlm
merged
2015-10-31, by wenzelm
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
2015-10-31, by wenzelm
global start time as reference point;
2015-10-31, by wenzelm
tuned signature -- clarified modules;
2015-10-30, by wenzelm
obsolete (see 9c6346319eee, 7924d61b50cf);
2015-10-30, by wenzelm
added splay trees
2015-10-30, by nipkow
added many small lemmas about setsum/setprod/powr/...
2015-10-29, by eberlm
no icons here -- not a standalone window;
2015-10-27, by wenzelm
workaround for problem with C-1, C-2, C-3 seen on Slovak QWERTY keyboard;
2015-10-27, by wenzelm
removed presumably obsolete workaround (see 7924d61b50cf);
2015-10-27, by wenzelm
Cauchy's integral formula, required lemmas, and a bit of reorganisation
2015-10-27, by paulson
merged
2015-10-26, by paulson
new lemmas about topology, etc., for Cauchy integral formula
2015-10-26, by paulson
adapted to 436b7fe89cdc
2015-10-26, by nipkow
clarified Latex.environment (again, amending e16649b70107): avoid additional paragraph, e.g. relevant for option [display];
2015-10-26, by wenzelm
added 234-trees (slow)
2015-10-25, by nipkow
added 234-Trees (slow)
2015-10-25, by nipkow
tuned
2015-10-25, by nipkow
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
2015-10-24, by wenzelm
updated to jedit-5.3.0 and SideKick 1.8;
2015-10-23, by wenzelm
updated to jdk-8u66;
2015-10-23, by wenzelm
print thm wrt. local shyps (from full proof context);
2015-10-23, by wenzelm
clarified modules;
2015-10-23, by wenzelm
proper transfer of stored facts;
2015-10-23, by wenzelm
tuned;
2015-10-22, by wenzelm
more robust ASCII output: avoid ligatures of quotes;
2015-10-22, by wenzelm
tuned;
2015-10-22, by wenzelm
more control symbols;
2015-10-22, by wenzelm
clarified scan_cartouche_depth (amending 8284c0d5bf52): finish after outermost cartouche;
2015-10-22, by wenzelm
rendering for \<^verbatim>;
2015-10-21, by wenzelm
Isabelle fonts via external component;
2015-10-21, by wenzelm
tuned document;
2015-10-21, by wenzelm
tuned document;
2015-10-21, by wenzelm
added glyphs 0x25a9 from DejaVuSansMono;
2015-10-21, by wenzelm
removed generated files from repository;
2015-10-21, by wenzelm
tuned;
2015-10-21, by wenzelm
proper spaces around @{text};
2015-10-21, by wenzelm
isabelle update_cartouches -t;
2015-10-20, by wenzelm
added isabelle update_cartouches option -t;
2015-10-20, by wenzelm
another antiquotation short form: undecorated cartouche as alias for @{text};
2015-10-20, by wenzelm
repaired document;
2015-10-19, by wenzelm
more symbols;
2015-10-19, by wenzelm
tuned English;
2015-10-19, by wenzelm
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
2015-10-19, by wenzelm
tuned document;
2015-10-19, by wenzelm
merged
2015-10-19, by wenzelm
avoid odd permissions of fresh tmp_file;
2015-10-19, by wenzelm
added action "isabelle-emph";
2015-10-19, by wenzelm
tuned;
2015-10-19, by wenzelm
tuned;
2015-10-19, by wenzelm
tuned text
2015-10-19, by nipkow
tuned;
2015-10-18, by wenzelm
merged
2015-10-18, by wenzelm
more control symbols;
2015-10-18, by wenzelm
tuned signature;
2015-10-18, by wenzelm
tuned signature;
2015-10-18, by wenzelm
clarified;
2015-10-18, by wenzelm
clarified control antiquotations: decode control symbol to get name;
2015-10-18, by wenzelm
more documentation;
2015-10-18, by wenzelm
support control symbol antiquotations;
2015-10-18, by wenzelm
clarified Symbol.is_control;
2015-10-18, by wenzelm
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
2015-10-18, by nipkow
code abbreviation for mapping over a fixed range
2015-10-17, by haftmann
back to lxbroy3, which appears to be free at the moment;
2015-10-17, by wenzelm
tuned signature;
2015-10-17, by wenzelm
merged
2015-10-17, by wenzelm
more uniform command setup;
2015-10-17, by wenzelm
added 'paragraph', 'subparagraph';
2015-10-17, by wenzelm
clarified Latex.environment;
2015-10-17, by wenzelm
more explicit output of list items;
2015-10-17, by wenzelm
tuned;
2015-10-17, by wenzelm
clarified nesting of paragraphs: indentation is taken into account more uniformly;
2015-10-17, by wenzelm
Markdown support in document text;
2015-10-16, by wenzelm
clarified Antiquote.antiq_reports;
2015-10-16, by wenzelm
trim_blanks after read, before eval;
2015-10-15, by wenzelm
clarified modules;
2015-10-15, by wenzelm
load markdown.ML into Pure;
2015-10-15, by wenzelm
proper recursive nesting of adjacent lists;
2015-10-15, by wenzelm
tuned;
2015-10-15, by wenzelm
clarified line content: source without marker prefix;
2015-10-15, by wenzelm
more markup;
2015-10-15, by wenzelm
report Markdown document structure;
2015-10-15, by wenzelm
more comments;
2015-10-15, by wenzelm
unused -- avoid confusion in Symbols dockable;
2015-10-15, by wenzelm
proper nesting of adjacent lists;
2015-10-15, by wenzelm
more document structure;
2015-10-15, by wenzelm
more document structure;
2015-10-14, by wenzelm
more document structure;
2015-10-14, by wenzelm
clarified;
2015-10-14, by wenzelm
minimal support for Markdown documents;
2015-10-14, by wenzelm
clarified;
2015-10-14, by wenzelm
more symbols;
2015-10-14, by wenzelm
more symbols;
2015-10-14, by wenzelm
clarified control symbols;
2015-10-14, by wenzelm
added glyphs 0x21e4, 0x21e5, 0x27a7 from DejaVuSansMono;
2015-10-14, by wenzelm
tuned signature (cf. XML.trim_blanks);
2015-10-13, by wenzelm
added split_lines;
2015-10-13, by wenzelm
qualify some names stemming from internal bootstrap constructions
2015-10-17, by haftmann
removed too aggressive underscorization
2015-10-15, by blanchet
typo
2015-10-13, by nipkow
prefer undecorated typedef
2015-10-13, by nipkow
even -> evn to avoid clash with global even
2015-10-13, by nipkow
added invar empty
2015-10-13, by nipkow
Fixed nonterminating "blast" proof
2015-10-13, by paulson
new material on path_component_sets, inside, outside, etc. And more default simprules
2015-10-13, by paulson
restored print translation from a1141fb798ff, to prevent a printing misfit observable using "thm divmod_nat_if" in theory "Divides", with a meagure indication in the comment
2015-10-13, by haftmann
prod_case as canonical name for product type eliminator
2015-10-13, by haftmann
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
tip