6 hours ago Lars Hupel 2018-01-23 drop redundant cong rules default tip
19 hours ago Lars Hupel 2018-01-22 merged
26 hours ago Lars Hupel 2018-01-22 drop redundant fundef_cong rule
26 hours ago Lars Hupel 2018-01-22 tuned
27 hours ago Lars Hupel 2018-01-22 repair malformed fundef_cong rule
27 hours ago nipkow 2018-01-22 removed duplicate
31 hours ago wenzelm 2018-01-22 tuned message: same error may occur in different contexts;
2 days ago wenzelm 2018-01-21 detect more errors;
2 days ago nipkow 2018-01-21 merged
2 days ago nipkow 2018-01-21 made sorted fun again
3 days ago nipkow 2018-01-20 imported patch sorted
3 days ago bulwahn 2018-01-20 add lemma on lists from Falling_Factorial_Sum entry
3 days ago wenzelm 2018-01-19 merged
3 days ago wenzelm 2018-01-19 avoid evaluation of embedded comment;
3 days ago wenzelm 2018-01-19 disable "display" style in marginal (line) comment;
3 days ago wenzelm 2018-01-19 more uniform output of source / text / theory_text, with handling of formal comments etc.;
4 days ago wenzelm 2018-01-19 sort completion result;
4 days ago wenzelm 2018-01-19 recovered antiquotation check without latex mode (cf. dfc93f2b01ea);
4 days ago wenzelm 2018-01-19 formal treatment of documentation names;
4 days ago wenzelm 2018-01-19 support for completion;
4 days ago wenzelm 2018-01-19 adapted to a5ca98950a91;
4 days ago wenzelm 2018-01-19 tuned output of plain name;
4 days ago wenzelm 2018-01-19 clarified signature;
4 days ago wenzelm 2018-01-19 tuned;
4 days ago wenzelm 2018-01-19 tuned;
4 days ago wenzelm 2018-01-18 unused;
4 days ago wenzelm 2018-01-18 clarified access to antiquotation options; define explicit variants of antiquotations; output proper Latex.text; misc tuning and clarification;
4 days ago wenzelm 2018-01-18 more operations;
6 days ago wenzelm 2018-01-17 tuned signature;
6 days ago wenzelm 2018-01-17 discontinued unused wrapper: print_mode is provided directly;
4 days ago nipkow 2018-01-19 corrected name
4 days ago nipkow 2018-01-19 moved from AFP/Gromov
4 days ago nipkow 2018-01-19 moved from AFP/Gromov
4 days ago nipkow 2018-01-19 added lemma
5 days ago nipkow 2018-01-18 moved from AFP/Gromov
5 days ago nipkow 2018-01-18 moved t3/t4 space from AFP/Gromov to here.
5 days ago nipkow 2018-01-18 more automation
6 days ago nipkow 2018-01-17 more lemmas by Gouezele
6 days ago nipkow 2018-01-17 move lemmas by Gouezel to distribution
6 days ago ballarin 2018-01-16 Experimental support for rewrite morphisms in locale instances.
7 days ago wenzelm 2018-01-16 tuned signature;
7 days ago wenzelm 2018-01-16 more documentation;
7 days ago wenzelm 2018-01-16 clarified markup;
7 days ago wenzelm 2018-01-16 discontinued old form of marginal comments;
7 days ago wenzelm 2018-01-16 tuned document;
7 days ago wenzelm 2018-01-16 clarified comments;
7 days ago wenzelm 2018-01-16 standardized towards new-style formal comments: isabelle update_comments;
7 days ago wenzelm 2018-01-16 uniform treatment of old-style and new-style comments;
7 days ago wenzelm 2018-01-16 tuned signature;
7 days ago wenzelm 2018-01-15 clarified markup;
7 days ago wenzelm 2018-01-15 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
8 days ago wenzelm 2018-01-15 clarified modules; more operations;
8 days ago nipkow 2018-01-15 tuned
8 days ago wenzelm 2018-01-14 eliminated clones;
8 days ago wenzelm 2018-01-14 trim blanks -- more thoroughly than in update_cartouches (for single-line comments);
8 days ago wenzelm 2018-01-14 more operations (as in ML);
8 days ago wenzelm 2018-01-14 more specific tool "isabelle update_comments", for uniformity with formal comments in embedded languages;
8 days ago wenzelm 2018-01-14 clarified Token.is_text (cf. Parse.text in ML);
8 days ago wenzelm 2018-01-14 more operations;
9 days ago wenzelm 2018-01-14 support for completion;