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.
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
emphasized general nature of parameter
2015-10-13, by haftmann
moved lemmas
2015-10-13, by haftmann
more symbols;
2015-10-12, by wenzelm
redundant due to \parindent 0pt;
2015-10-12, by wenzelm
isabelle update_cartouches;
2015-10-12, by wenzelm
scalable fonts for T1 encoding;
2015-10-12, by wenzelm
proper imports;
2015-10-12, by wenzelm
more symbols;
2015-10-12, by wenzelm
more symbols;
2015-10-12, by wenzelm
more antiquotations;
2015-10-12, by wenzelm
proper message;
2015-10-12, by wenzelm
clarified antiquotation;
2015-10-12, by wenzelm
spelling;
2015-10-12, by wenzelm
unused;
2015-10-12, by wenzelm
obsolete;
2015-10-12, by wenzelm
@{verbatim [display]} supersedes old alltt/ttbox;
2015-10-12, by wenzelm
@{verbatim [display]} supersedes old alltt/ttbox;
2015-10-12, by wenzelm
more symbols;
2015-10-12, by wenzelm
some control symbols for markup and formatting;
2015-10-12, by wenzelm
allow control symbols within markup body;
2015-10-12, by wenzelm
added glyphs 0x2501, 0x2508, 0x2509, 0x25aa, 0x25b8 from DejaVuSansMono;
2015-10-12, by wenzelm
proper document source;
2015-10-11, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned syntax -- less symbols;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned whitespace;
2015-10-10, by wenzelm
tuned;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
more symbols;
2015-10-10, by wenzelm
more symbols;
2015-10-10, by wenzelm
more symbols;
2015-10-10, by wenzelm
prefer symbols;
2015-10-10, by wenzelm
use Isabelle symbols by default;
2015-10-10, by wenzelm
isabelle update_cartouches;
2015-10-10, by wenzelm
more explicit HTML.symbols;
2015-10-10, by wenzelm
NEWS;
2015-10-09, by wenzelm
more direct HTML presentation, without print mode;
2015-10-09, by wenzelm
discontinued specific HTML syntax;
2015-10-09, by wenzelm
installable TTF for MS IE 9+;
2015-10-09, by wenzelm
output HTML text according to Isabelle/Scala Symbol.Interpretation;
2015-10-09, by wenzelm
tuned output;
2015-10-09, by wenzelm
server-side fonts;
2015-10-09, by wenzelm
more accurate imitation of "cp -p -f";
2015-10-09, by wenzelm
more Present operations on Scala side;
2015-10-09, by wenzelm
clarified, according to Isabelle_System.copy_file in ML;
2015-10-09, by wenzelm
NEWS
2015-10-09, by kuncar
documentation for transfer debug methods
2015-10-09, by kuncar
add a file with examples of debugging transfer
2015-10-09, by kuncar
new methods for debugging transfer and transfer_prover
2015-10-09, by kuncar
right parenthesization
2015-10-09, by kuncar
made TPTP SZS status more compliant
2015-10-08, by blanchet
tuning
2015-10-08, by blanchet
measurable sets on product spaces are embeddings of countable products
2015-10-08, by hoelzl
generalize eqI theorems for product measures
2015-10-08, by hoelzl
isabelle update_cartouches;
2015-10-07, by wenzelm
more glyphs from DejaVuSansMono and DejaVuSansMono-Bold: 0100-017F Latin Extended-A, 0180-024F Latin Extended-B;
2015-10-07, by wenzelm
cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
2015-10-07, by hoelzl
avoid 'legacy binding' warning
2015-10-07, by blanchet
removed dead code
2015-10-07, by blanchet
merged
2015-10-07, by wenzelm
back to old-fashioned GC, which appears to work better with interactive applications;
2015-10-07, by wenzelm
routine check of theory context;
2015-08-31, by wenzelm
proper context;
2015-10-06, by wenzelm
proper context;
2015-10-06, by wenzelm
clarify docs
2015-10-07, by blanchet
updated docs
2015-10-07, by blanchet
made documentation more accurate
2015-10-07, by blanchet
disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier
2015-10-07, by blanchet
avoid unsound 'nitpick_simp' attribute on nonterminating, nonproductive equations
2015-10-06, by blanchet
parallel tests: 6h & 12h;
2015-10-06, by wenzelm
news
2015-10-06, by blanchet
generate 'case_transfer' unconditionally
2015-10-06, by blanchet
isabelle update_cartouches;
2015-10-06, by wenzelm
isabelle update_cartouches;
2015-10-06, by wenzelm
merged
2015-10-06, by wenzelm
avoid hardwired frees;
2015-10-06, by wenzelm
added Thm.forall_intr_name;
2015-10-06, by wenzelm
added 'proposition' command;
2015-10-06, by wenzelm
fewer aliases for toplevel theorem statements;
2015-10-06, by wenzelm
just one theorem kind, which is legacy anyway;
2015-10-06, by wenzelm
pretty_const: proper local name space;
2015-10-06, by wenzelm
collect the names from goals in favor of fragile exports
2015-10-06, by traytel
compile
2015-10-06, by blanchet
tuning
2015-10-06, by blanchet
avoid legacy syntax
2015-10-06, by blanchet
further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes
2015-10-05, by blanchet
added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
2015-10-05, by blanchet
merged
2015-10-05, by wenzelm
tuned signature;
2015-10-05, by wenzelm
produce nodes_status outside GUI thread, to avoid a few milliseconds of blocking;
2015-10-05, by wenzelm
avoid too aggressive optimization of 'finite' predicate
2015-10-05, by blanchet
avoid unsound simplification of (C (s x)) when s is a selector but not C's
2015-10-05, by blanchet
extended theory exporter to also export MePo-selected facts
2015-10-05, by blanchet
speed up MaSh duplicate check
2015-10-04, by blanchet
sped up MaSh nickname generation
2015-10-04, by blanchet
merged
2015-10-03, by wenzelm
more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod -w for heap images;
2015-10-02, by wenzelm
speed up MaSh
2015-10-03, by blanchet
updated docs and NEWS
2015-10-02, by blanchet
updated docs
2015-10-02, by blanchet
removed Nitpick nonblocking mode, that was never really used
2015-10-02, by blanchet
adapted example
2015-10-02, by blanchet
removed obsolete material in documentation
2015-10-02, by blanchet
further reduced dependency on legacy async thread manager
2015-10-02, by blanchet
removed legacy asynchronous mode in Sledgehammer
2015-10-02, by blanchet
better compliance with TPTP SZS standard
2015-10-02, by blanchet
merged
2015-10-02, by wenzelm
avoid useless empty case_names;
2015-10-02, by wenzelm
clarified init (again): isabelle.Main is responsible to provide basic JVM setup, jedit.jar picks this up (e.g. list of known fonts), plugin cannot be loaded in isolation without isabelle.Main;
2015-10-02, by wenzelm
New theorems about connected sets. And pairwise moved to Set.thy.
2015-10-02, by paulson
less ambitious regex -- avoid unclarities of escaping;
2015-10-01, by wenzelm
tuned documentation
2015-10-01, by blanchet
tuned datatype docs
2015-10-01, by blanchet
export proof method in signature
2015-10-01, by blanchet
export '_cmd' functions
2015-10-01, by blanchet
back to old JavaAppLauncher to avoid initial startup problems (due to unsigned application?);
2015-09-30, by wenzelm
tuned GUI;
2015-09-30, by wenzelm
proper isabelle.root for bootstrap;
2015-09-30, by wenzelm
merged
2015-09-30, by wenzelm
tuned;
2015-09-30, by wenzelm
proper Cygwin.init (amending e00e1bf23d03);
2015-09-30, by wenzelm
renamed jvmpath to platform_path;
2015-09-30, by wenzelm
clarified ISABELLE_ROOT (platform path) vs. ISABELLE_HOME (standard path);
2015-09-30, by wenzelm
tuned GUI;
2015-09-30, by wenzelm
uniform treatment of bootstrap directories;
2015-09-30, by wenzelm
more robust system init (again), in case the plugin is started without isabelle.Main;
2015-09-30, by wenzelm
tuned message;
2015-09-30, by wenzelm
clarified modules;
2015-09-30, by wenzelm
Merge
2015-09-30, by paulson
Dead wood removal
2015-09-30, by paulson
Merge
2015-09-30, by paulson
real_of_nat_Suc is now a simprule
2015-09-30, by paulson
updated docs
2015-09-30, by blanchet
clarified Isabelle_System.init;
2015-09-29, by wenzelm
tuned;
2015-09-29, by wenzelm
tuned GUI;
2015-09-29, by wenzelm
proper event;
2015-09-29, by wenzelm
tuned GUI;
2015-09-29, by wenzelm
build session within running jEdit;
2015-09-29, by wenzelm
clarified modules;
2015-09-29, by wenzelm
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
2015-09-27, by haftmann
more selective preprocessing allows bare "numeral" occurences to be retained as real function in generated code
2015-09-27, by haftmann
Caratheodory: cleanup and modernisation
2015-09-28, by hoelzl
restructure fresh variable generation to make exports more wellformed
2015-09-25, by traytel
more canonical context threading
2015-09-25, by traytel
merged
2015-09-25, by wenzelm
documentation for "Semantic subtype definitions";
2015-09-25, by wenzelm
moved remaining display.ML to more_thm.ML;
2015-09-25, by wenzelm
less redundant output;
2015-09-25, by wenzelm
proper context;
2015-09-25, by wenzelm
tuned;
2015-09-25, by wenzelm
tuned;
2015-09-25, by wenzelm
tuned;
2015-09-25, by wenzelm
tuned signature: eliminated pointless type Context.pretty;
2015-09-25, by wenzelm
more explicit Defs.context: use proper name spaces as far as possible;
2015-09-24, by wenzelm
explicit indication of overloaded typedefs;
2015-09-24, by wenzelm
tuned signature;
2015-09-23, by wenzelm
tuned output;
2015-09-23, by wenzelm
tuned output;
2015-09-23, by wenzelm
tuned signature;
2015-09-22, by wenzelm
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
2015-09-22, by wenzelm
tuned signature;
2015-09-22, by wenzelm
tuned output;
2015-09-22, by wenzelm
separate command 'print_definitions';
2015-09-22, by wenzelm
tuned;
2015-09-22, by wenzelm
clarified deps entry: global names for arguments;
2015-09-22, by wenzelm
renamed Defs.node to Defs.item;
2015-09-22, by wenzelm
tuned signature;
2015-09-22, by wenzelm
tuned whitespace;
2015-09-22, by wenzelm
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
2015-09-22, by wenzelm
prove Liminf_inverse_ereal
2015-09-25, by hoelzl
merged
2015-09-24, by immler
exchange uniform limit and integral
2015-09-24, by immler
congruence rules for the relator
2015-09-24, by traytel
conceal only the definitional theorems of map, set, rel (and not the actual constants)
2015-09-24, by traytel
more useful properties of the relators
2015-09-24, by traytel
tuned proofs (less warnings)
2015-09-24, by traytel
Useful facts about min/max, etc.
2015-09-23, by paulson
Merge
2015-09-23, by paulson
fixed a VERY SLOW proof
2015-09-23, by paulson
SOME rather than THE makes it easy to prove equivalence with other forms of derivatives
2015-09-22, by paulson
New lemmas
2015-09-22, by paulson
Prepared two non-terminating proofs; no obvious link with my changes
2015-09-22, by paulson
added AVL and lookup function
2015-09-23, by nipkow
tuned
2015-09-23, by nipkow
merged
2015-09-22, by nipkow
unified isin-proofs
2015-09-22, by nipkow
tuned
2015-09-22, by haftmann
include some data structures into code generation
2015-09-22, by haftmann
effective revert of e6b1236f9b3d: spontaneous eta-contraction happens on the print translation level and can only be suppressed on the print translation level
2015-09-22, by haftmann
tuned references
2015-09-22, by nipkow
added red black trees
2015-09-22, by nipkow
clarified markup;
2015-09-21, by wenzelm
isabelle update_cartouches;
2015-09-21, by wenzelm
merged
2015-09-21, by wenzelm
tuned GUI;
2015-09-21, by wenzelm
removed auto update -- bad reactivity;
2015-09-21, by wenzelm
clarified isabelle.update-state;
2015-09-21, by wenzelm
more reactive update, like Output panel;
2015-09-21, by wenzelm
added isabelle update_then;
2015-09-21, by wenzelm
NEWS;
2015-09-21, by wenzelm
tuned priority (like other query operations, e.g. "find_theorems");
2015-09-21, by wenzelm
option editor_output_state;
2015-09-21, by wenzelm
obsolete, superseded by State panel;
2015-09-21, by wenzelm
added action "isabelle-update-state";
2015-09-21, by wenzelm
support for auto update via caret focus;
2015-09-21, by wenzelm
tuned signature;
2015-09-21, by wenzelm
separate panel for proof state output;
2015-09-21, by wenzelm
tuned;
2015-09-21, by wenzelm
more specific name to reduce danger of clash with direct uses of plain Command.print_function;
2015-09-21, by wenzelm
tuned;
2015-09-21, by wenzelm
new lemmas and movement of lemmas into place
2015-09-21, by paulson
New subdirectory for functional data structures
2015-09-21, by nipkow
Added new simplifier predicate ASSUMPTION
2015-09-21, by nipkow
eliminated suspicious unicode;
2015-09-19, by wenzelm
eliminated hard tabs;
2015-09-19, by wenzelm
obsolete;
2015-09-19, by wenzelm
NEWS;
2015-09-19, by wenzelm
straight-forward refresh, without special preconditions;
2015-09-19, by wenzelm
eliminated pointless jedit_text_overview_limit;
2015-09-19, by wenzelm
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
2015-09-19, by wenzelm
allow to cancel running event;
2015-09-19, by wenzelm
tuned;
2015-09-19, by wenzelm
tuned signature;
2015-09-19, by wenzelm
Merge
2015-09-18, by paulson
Massive revisions, as a valid path must now be continously differentiable (C!)
2015-09-18, by paulson
isabelle update_cartouches;
2015-09-17, by wenzelm
isabelle update_cartouches;
2015-09-17, by wenzelm
recode all text, which is relevant for Session.save on non-ASCII directory;
2015-09-16, by wenzelm
tuned;
2015-09-16, by wenzelm
more recent JavaAppLauncher, which supports file associations;
2015-09-16, by wenzelm
more explicit indication of bundled jdk, which is required for newer versions of JavaAppLauncher;
2015-09-16, by wenzelm
more app properties glimpsed from infinitekind/Moneydance 2015.5;
2015-09-16, by wenzelm
tuned whitespace;
2015-09-16, by wenzelm
updated to polyml-5.5.3-20150916 (polyml git version cb1b36caa242);
2015-09-16, by wenzelm
avoid module dependency cycles
2015-09-15, by Andreas Lochbihler
goali -> i
2015-09-15, by nipkow
Omega_Words_Fun: Infinite words as functions from nat.
2015-09-15, by lammich
provide FontMapper for embedded fonts;
2015-09-14, by wenzelm
avoid hardwired colors;
2015-09-14, by wenzelm
avoid hardwired colors;
2015-09-14, by wenzelm
replacement character for spaces;
2015-09-14, by wenzelm
single-instance application, even on Linux;
2015-09-14, by wenzelm
single-instance application for Linux;
2015-09-14, by wenzelm
tuned message;
2015-09-14, by wenzelm
added isabelle jedit_client;
2015-09-14, by wenzelm
tuned proofs -- less legacy;
2015-09-13, by wenzelm
tuned message;
2015-09-13, by wenzelm
tuned proofs;
2015-09-13, by wenzelm
renamed method "goals" to "goal_cases" to emphasize its meaning;
2015-09-13, by wenzelm
tuned proofs;
2015-09-13, by wenzelm
method "goals" ignores facts;
2015-09-13, by wenzelm
tuned;
2015-09-13, by wenzelm
unconceal symbols stemming from inductive_set specifications, which are regular part of user-space specification;
2015-09-10, by haftmann
fully detached test run, to avoid flashing window on Windows with Cygwin-Terminal;
2015-09-11, by wenzelm
single-instance application on Windows;
2015-09-11, by wenzelm
more robust init_components: test run of polyml executable on windows appears to disrupt stdin stream of cygwin;
2015-09-11, by wenzelm
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
2015-09-11, by wenzelm
clarified order;
2015-09-11, by wenzelm
more symbols;
2015-09-11, by wenzelm
Unicode is standard in Poly/ML repository version;
2015-09-10, by wenzelm
removed obsolete undocumented feature;
2015-09-10, by wenzelm
more standard local_theory operations;
2015-09-10, by wenzelm
HOL-Proofs is slow;
2015-09-10, by wenzelm
convenient access to application properties;
2015-09-10, by wenzelm
tuned -- avoid slightly odd @{cpat};
2015-09-10, by wenzelm
dropped redundant NEWS
2015-09-10, by haftmann
less ambitious options, to accomodate 4GB systems;
2015-09-10, by wenzelm
tuned
2015-09-10, by nipkow
clarified declaration flags, like 'declaration' command;
2015-09-09, by wenzelm
merged
2015-09-09, by wenzelm
simplified simproc programming interfaces;
2015-09-09, by wenzelm
eliminated \<Colon> from syntax of constraints;
2015-09-09, by wenzelm
eliminated \<Colon> -- from dead code!
2015-09-09, by wenzelm
merged
2015-09-09, by Andreas Lochbihler
reactivate examples with predicate compiler and quickcheck
2015-09-09, by Andreas Lochbihler
disable jedit_auto_resolve (again) -- too confusing;
2015-09-08, by wenzelm
proper Windows path, notably for ML basis;
2015-09-08, by wenzelm
more basic Windows path operations -- evade exception InvalidArc with Unicode;
2015-09-08, by wenzelm
updated to polyml-5.5.3-20150908, with support for x86_64-windows and Unicode file-names;
2015-09-08, by wenzelm
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
2015-09-08, by wenzelm
clarified Java runtime options for 32 vs. 64 bit;
2015-09-08, by wenzelm
clarified JEDIT_JAVA_OPTIONS: separate defaults for 32 vs. 64 bit;
2015-09-08, by wenzelm
clarified JEDIT_JAVA_SYSTEM_OPTIONS;
2015-09-08, by wenzelm
clarified ISABELLE_BUILD_JAVA_OPTIONS;
2015-09-08, by wenzelm
unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup
2015-09-06, by haftmann
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
2015-09-06, by haftmann
formally regenerated
2015-09-06, by haftmann
tuned notation, proofs, namespace
2015-09-06, by haftmann
obsolete: if case_prod is fully applied, it is printed as proper case expression;
2015-09-06, by haftmann
prefer "uncurry" as canonical name for case distinction on products in combinatorial view
2015-09-06, by haftmann
tuned
2015-09-06, by haftmann
obsolete: all (formally unchecked) examples given in the comments work out of the box as advertised
2015-09-06, by haftmann
dropped whitespace leftover from b57df8eecad6
2015-09-06, by haftmann
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
2015-09-06, by wenzelm
tuned proofs;
2015-09-06, by wenzelm
removed obsolete theory Legacy_Mrec;
2015-09-06, by wenzelm
NEWS;
2015-09-06, by wenzelm
merged
2015-09-04, by wenzelm
close derivation *before* splitting conjuncts, like Goal.prove_common (see also 757cad5a3fe9) -- potential improvement of performance;
2015-09-04, by wenzelm
modernized name space management -- more uniform qualification;
2015-09-04, by wenzelm
tuned -- do not open ML structures;
2015-09-04, by wenzelm
trim context for persistent storage;
2015-09-04, by wenzelm
trim context for persistent storage;
2015-09-04, by wenzelm
proper restore naming after close, which is important for packages that used nested targets internally, e.g. BNF datatype;
2015-09-04, by wenzelm
more general Typedef.bindings;
2015-09-03, by wenzelm
proper restore_naming after global qed, which is important to make Name_Space.transform_naming work properly, e.g. for "private typedef";
2015-09-03, by wenzelm
merged
2015-09-04, by Andreas Lochbihler
merged
2015-09-03, by Andreas Lochbihler
use quotient and lifting package;
2015-09-03, by Andreas Lochbihler
merged
2015-09-03, by paulson
new lemmas about vector_derivative, complex numbers, paths, etc.
2015-09-03, by paulson
trim context for persistent storage;
2015-09-03, by wenzelm
misc tuning and modernization;
2015-09-03, by wenzelm
use open/close_target rather than Local_Theory.restore to get polymorphic definitions;
2015-09-03, by traytel
clean name as in ML Completion.make;
2015-09-03, by wenzelm
use alphabetic order before history order;
2015-09-03, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
tip