isabelle: Graph

made sorted fun again
2018-01-21, by nipkow
imported patch sorted
2018-01-20, by nipkow
add lemma on lists from Falling_Factorial_Sum entry
2018-01-20, by bulwahn
merged
2018-01-19, by wenzelm
avoid evaluation of embedded comment;
2018-01-19, by wenzelm
disable "display" style in marginal (line) comment;
2018-01-19, by wenzelm
more uniform output of source / text / theory_text, with handling of formal comments etc.;
2018-01-19, by wenzelm
sort completion result;
2018-01-19, by wenzelm
recovered antiquotation check without latex mode (cf. dfc93f2b01ea);
2018-01-19, by wenzelm
formal treatment of documentation names;
2018-01-19, by wenzelm
support for completion;
2018-01-19, by wenzelm
adapted to a5ca98950a91;
2018-01-19, by wenzelm
tuned output of plain name;
2018-01-19, by wenzelm
clarified signature;
2018-01-19, by wenzelm
tuned;
2018-01-19, by wenzelm
tuned;
2018-01-19, by wenzelm
unused;
2018-01-18, by wenzelm
clarified access to antiquotation options;
2018-01-18, by wenzelm
more operations;
2018-01-18, by wenzelm
tuned signature;
2018-01-17, by wenzelm
discontinued unused wrapper: print_mode is provided directly;
2018-01-17, by wenzelm
corrected name
2018-01-19, by nipkow
moved from AFP/Gromov
2018-01-19, by nipkow
moved from AFP/Gromov
2018-01-19, by nipkow
added lemma
2018-01-19, by nipkow
moved from AFP/Gromov
2018-01-18, by nipkow
moved t3/t4 space from AFP/Gromov to here.
2018-01-18, by nipkow
more automation
2018-01-18, by nipkow
more lemmas by Gouezele
2018-01-17, by nipkow
move lemmas by Gouezel to distribution
2018-01-17, by nipkow
Experimental support for rewrite morphisms in locale instances.
2018-01-16, by ballarin
tuned signature;
2018-01-16, by wenzelm
more documentation;
2018-01-16, by wenzelm
clarified markup;
2018-01-16, by wenzelm
discontinued old form of marginal comments;
2018-01-16, by wenzelm
tuned document;
2018-01-16, by wenzelm
clarified comments;
2018-01-16, by wenzelm
standardized towards new-style formal comments: isabelle update_comments;
2018-01-16, by wenzelm
uniform treatment of old-style and new-style comments;
2018-01-16, by wenzelm
tuned signature;
2018-01-16, by wenzelm
clarified markup;
2018-01-15, by wenzelm
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
2018-01-15, by wenzelm
clarified modules;
2018-01-15, by wenzelm
tuned
2018-01-15, by nipkow
eliminated clones;
2018-01-14, by wenzelm
trim blanks -- more thoroughly than in update_cartouches (for single-line comments);
2018-01-14, by wenzelm
more operations (as in ML);
2018-01-14, by wenzelm
more specific tool "isabelle update_comments", for uniformity with formal comments in embedded languages;
2018-01-14, by wenzelm
clarified Token.is_text (cf. Parse.text in ML);
2018-01-14, by wenzelm
more operations;
2018-01-14, by wenzelm
support for completion;
2018-01-14, by wenzelm
allow LaTeX source as formal comment;
2018-01-14, by wenzelm
clarified signature;
2018-01-14, by wenzelm
clarified SML (no formal comments) vs. Isabelle/ML (arbitrary comments);
2018-01-14, by wenzelm
clarified signature;
2018-01-14, by wenzelm
clarified modules: uniform notion of formal comments;
2018-01-14, by wenzelm
added glyph from "Deja Vu Sans Mono" font;
2018-01-13, by wenzelm
tuned messages;
2018-01-13, by wenzelm
merged
2018-01-13, by wenzelm
allow TeX comment % in formal comment body, but avoid extra space (cf. d7c6054b2ab1);
2018-01-13, by wenzelm
tuned;
2018-01-13, by wenzelm
tuned;
2018-01-13, by wenzelm
more general error suffixes, e.g. for messages that are broken over several lines;
2018-01-13, by wenzelm
another Latex error seen in the wild:
2018-01-13, by wenzelm
clarified default;
2018-01-13, by wenzelm
clarified formal comments;
2018-01-13, by wenzelm
prefer formal comments;
2018-01-13, by wenzelm
added \<^cancel> operator for unused text;
2018-01-13, by wenzelm
tuned;
2018-01-12, by wenzelm
restored naming of lemmas after corresponding constants
2018-01-13, by haftmann
prefer formal comments;
2018-01-12, by wenzelm
prefer formal text;
2018-01-12, by wenzelm
prefer formal comments;
2018-01-12, by wenzelm
prefer formal comments;
2018-01-12, by wenzelm
isabelle update_cartouches -c;
2018-01-12, by wenzelm
uniform use of Standard ML op-infix -- eliminated warnings;
2018-01-11, by wenzelm
proper infix;
2018-01-11, by wenzelm
line break before op was intentional
2018-01-11, by nipkow
typo
2018-01-10, by nipkow
tuned notation
2018-01-10, by nipkow
tuned
2018-01-10, by nipkow
ran isabelle update_op on all sources
2018-01-10, by nipkow
Manual updates towards conversion of "op" syntax
2018-01-10, by nipkow
tuned op
2018-01-10, by nipkow
tuned op's
2018-01-10, by nipkow
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
2018-01-09, by wenzelm
uniform typesetting of \isamarkupcmt and \isasymcomment;
2018-01-09, by wenzelm
more accurate position for enclosing cartouche;
2018-01-09, by wenzelm
tuned;
2018-01-09, by wenzelm
clarified signature;
2018-01-09, by wenzelm
clarified presentation_state with provide presentation_context;
2018-01-09, by wenzelm
show only symbols with code;
2018-01-09, by wenzelm
clarified markup: more like outer syntax side-comment;
2018-01-09, by wenzelm
clarified rail token language: white space and formal comments;
2018-01-09, by wenzelm
clarified modules;
2018-01-09, by wenzelm
removed duplicate text;
2018-01-09, by wenzelm
clarified exception;
2018-01-09, by wenzelm
merged;
2018-01-09, by wenzelm
updated to 146757999c8d;
2018-01-09, by wenzelm
theory Pure is default presentation context;
2018-01-08, by wenzelm
clarified implicit Pure.thy;
2018-01-08, by wenzelm
prefer qualified names;
2018-01-08, by wenzelm
tuned;
2018-01-08, by wenzelm
check formal comments recursively, within arbitrary cartouches (unknown sublanguages);
2018-01-08, by wenzelm
more operations;
2018-01-08, by wenzelm
tuned;
2018-01-08, by wenzelm
clarified output (see also 909dcdec2122, 34d1913f0b20);
2018-01-08, by wenzelm
more operations;
2018-01-08, by wenzelm
tuned;
2018-01-08, by wenzelm
moved in some material from Euler-MacLaurin
2018-01-08, by paulson
merged
2018-01-07, by wenzelm
prefer formal comments;
2018-01-07, by wenzelm
clarified NEWS;
2018-01-07, by wenzelm
tuned whitespace;
2018-01-07, by wenzelm
tuned;
2018-01-07, by wenzelm
support for formal comments in ML in Isabelle/Scala;
2018-01-07, by wenzelm
tuned;
2018-01-07, by wenzelm
tuned message;
2018-01-07, by wenzelm
allow formal comments in ML;
2018-01-07, by wenzelm
clarified modules;
2018-01-07, by wenzelm
tuned;
2018-01-07, by wenzelm
more uniform output: formal comments within {* ... *};
2018-01-07, by wenzelm
tuned;
2018-01-07, by wenzelm
clarified output: avoid extra space;
2018-01-07, by wenzelm
output token content with formal comments and antiquotations;
2018-01-07, by wenzelm
tuned;
2018-01-07, by wenzelm
clarified signature;
2018-01-06, by wenzelm
clarified modules;
2018-01-06, by wenzelm
inner syntax comments may be written as "\<comment> \<open>text\<close>";
2018-01-06, by wenzelm
spelling
2018-01-07, by haftmann
corrected op
2018-01-06, by nipkow
tuned op
2018-01-06, by nipkow
tuned op
2018-01-06, by nipkow
tuned op
2018-01-06, by nipkow
tuned op
2018-01-06, by nipkow
tuned op's
2018-01-06, by nipkow
tuned op
2018-01-06, by nipkow
tuned op
2018-01-06, by nipkow
tuned op's
2018-01-05, by nipkow
Renamed (^) to [^] in preparation of the move from "op X" to (X)
2018-01-05, by nipkow
tuned op
2018-01-05, by nipkow
HOL-Analysis: add set_integrable_restrict_space
2018-01-04, by hoelzl
more correct parentheses
2018-01-03, by haftmann
more tight HTML output: avoid extra lines within <pre>;
2018-01-03, by wenzelm
HTML output for Markdown elements;
2018-01-03, by wenzelm
updated NEWS
2018-01-03, by blanchet
removed dead code
2018-01-03, by blanchet
removed old 'add_datatype' ML functions
2018-01-03, by blanchet
kill old size infrastructure
2018-01-03, by blanchet
repaired whitespace accident from 2505cabfc515
2018-01-02, by haftmann
proper namespace for evaluators
2018-01-01, by haftmann
tuned
2018-01-01, by haftmann
more correct name resolving
2018-01-01, by haftmann
skip abstract constructors silently in datatype clauses of computations
2018-01-01, by haftmann
removed para about 'old_datatype' in docs
2018-01-02, by blanchet
old_datatype no longer exists (cf. 706b1cf7b76d);
2018-01-02, by wenzelm
merged
2018-01-02, by wenzelm
PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);
2018-01-02, by wenzelm
clarified terminology of "markdown_bullet";
2018-01-02, by wenzelm
compile
2018-01-02, by blanchet
updated dependencies + compile
2018-01-02, by blanchet
moved 'realizers' into their own theory, now that they are decupled from the old datatype construction
2018-01-02, by blanchet
removed 'old_datatype' command
2018-01-02, by blanchet
don't test 'old_datatype', which is on its way out
2018-01-02, by blanchet
ported inductive realizer to new datatype package
2018-01-02, by blanchet
removed needless theorems
2018-01-02, by blanchet
store high-level 'size' equations
2018-01-02, by blanchet
avoid call to function that may throw an exception in error message
2018-01-02, by blanchet
misc tuning and modernization;
2018-01-01, by wenzelm
more completion templates;
2018-01-01, by wenzelm
proper purge of auxiliary bibtex theory;
2018-01-01, by wenzelm
tuned signature;
2018-01-01, by wenzelm
tuned;
2018-01-01, by wenzelm
Restored correct spacing for set comprehensions
2017-12-31, by paulson
less redundant;
2017-12-30, by wenzelm
more robust hyphen (see also "Soft hyphen (SHY) – a hard problem?" http://jkorpela.fi/shy.html);
2017-12-30, by wenzelm
more robust treatment of conflicts with existing Unicode text;
2017-12-30, by wenzelm
tuned whitespace;
2017-12-30, by wenzelm
no check for bibtex entries from other sessions;
2017-12-29, by wenzelm
clarified signature;
2017-12-29, by wenzelm
more accurate message patterns;
2017-12-29, by wenzelm
prefer formal citations;
2017-12-29, by wenzelm
proper bibtex entries;
2017-12-29, by wenzelm
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
2017-12-29, by wenzelm
clarified check, notably for bibtex theory (amending 5f082b1fa9fa);
2017-12-28, by wenzelm
NEWS;
2017-12-28, by wenzelm
proper check for imports, not just ROOT entries;
2017-12-28, by wenzelm
tuned signature;
2017-12-28, by wenzelm
implicit thy_load context for bibtex files (VSCode);
2017-12-28, by wenzelm
bibtex theory is always required and thus eventually consolidated;
2017-12-28, by wenzelm
implicit thy_load context for bibtex files;
2017-12-28, by wenzelm
clarified signature: prefer Document.Node.Name.is_bibtex;
2017-12-28, by wenzelm
avoid spurious noise: Prover IDE is meant to check for errors;
2017-12-28, by wenzelm
clarified signature;
2017-12-28, by wenzelm
avoid clash with special files in HTML output;
2017-12-28, by wenzelm
unused;
2017-12-28, by wenzelm
tuned signature;
2017-12-28, by wenzelm
prefer existing Resources.check_path;
2017-12-28, by wenzelm
more accurate bibtex entries;
2017-12-28, by wenzelm
added command 'bibtex_file' (for PIDE interaction only);
2017-12-28, by wenzelm
clarified default position for empty message pos;
2017-12-27, by wenzelm
spelling
2017-12-25, by haftmann
Removed Analysis/ex/Circle_Area; replaced by more general Analysis/Ball_Volume
2017-12-24, by eberlm
fewer warnings;
2017-12-24, by wenzelm
clarified positions;
2017-12-24, by wenzelm
check bibtex database on ML side -- for semantic PIDE editing;
2017-12-24, by wenzelm
clarified directories;
2017-12-24, by wenzelm
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
2017-12-24, by wenzelm
check bibtex database: errors and warnings;
2017-12-23, by wenzelm
more symbols;
2017-12-23, by wenzelm
Merge
2017-12-22, by paulson
Merge
2017-12-22, by paulson
new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product
2017-12-22, by paulson
more symbols;
2017-12-22, by wenzelm
tuned;
2017-12-22, by wenzelm
store full blob source for the sake of markup_to_XML;
2017-12-22, by wenzelm
PIDE markup for non-theory nodes;
2017-12-22, by wenzelm
discontinued 'display_drafts' command;
2017-12-22, by wenzelm
action "isabelle.draft" for plain-text preview;
2017-12-22, by wenzelm
NEWS;
2017-12-22, by wenzelm
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
2017-12-22, by wenzelm
tuned;
2017-12-22, by wenzelm
clarified URL: unique node name;
2017-12-22, by wenzelm
clarified signature;
2017-12-22, by wenzelm
proper title;
2017-12-22, by wenzelm
HTML rendering of \<^control> as in Isabelle/jEdit;
2017-12-22, by wenzelm
auto update;
2017-12-22, by wenzelm
clarified modules;
2017-12-22, by wenzelm
proper HTML title;
2017-12-22, by wenzelm
tuned signature;
2017-12-22, by wenzelm
tuned output;
2017-12-21, by wenzelm
merged
2017-12-21, by wenzelm
isabelle.preview presents bibtex database files as well;
2017-12-21, by wenzelm
clarified signature;
2017-12-21, by wenzelm
isabelle.preview presents auxiliary text files as well;
2017-12-21, by wenzelm
tuned signature;
2017-12-21, by wenzelm
tuned signature;
2017-12-21, by wenzelm
bibtex HTML output via external tool;
2017-12-21, by wenzelm
merged
2017-12-21, by nipkow
tuned op's
2017-12-21, by nipkow