13 months ago wenzelm 2019-04-28 tuned signature;
13 months ago haftmann 2019-04-17 backed out experimental b67bab2b132c, which slipped in accidentally
13 months ago haftmann 2019-04-16 hierarchically inclusive named theorem collections
13 months ago wenzelm 2019-04-13 more abbrevs;
13 months ago wenzelm 2019-04-04 tuned;
13 months ago wenzelm 2019-04-04 type Path.binding may be empty: check later via proper_binding; clarified 'export_prefix' default;
13 months ago wenzelm 2019-04-04 clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure; tuned concrete syntax;
13 months ago wenzelm 2019-04-04 added command 'compile_generated_files'; tuned signature;
13 months ago wenzelm 2019-04-03 clarified signature: more explicit operations for corresponding Isar commands;
14 months ago wenzelm 2019-03-28 "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports; "export_code ... file" is legacy, the empty name form has been discontinued; updated examples;
14 months ago wenzelm 2019-03-14 more specific keyword kinds;
14 months ago wenzelm 2019-03-10 document markers are formal comments, and may thus occur anywhere in the command-span; clarified Outer_Syntax.parse_span, Outer_Syntax.parse_text wrt. span structure; tuned signature;
14 months ago wenzelm 2019-03-10 added semantic document markers; emulate old-style tags as "tag" markers, with subtle change of semantics for multiples tags (ever used?); tuned;
16 months ago wenzelm 2019-01-15 added command 'export_generated_files'; clarified signature;
17 months ago haftmann 2018-12-20 disregard historic keyword
18 months ago wenzelm 2018-12-01 clarified modules;
18 months ago wenzelm 2018-11-30 more general command 'generate_file' for registered file types, notably Haskell; discontinued 'generate_haskell_file', 'export_haskell_file'; eliminated generated sources: compile files in tmp dir;
18 months ago wenzelm 2018-11-27 more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups; tuned signature;
18 months ago wenzelm 2018-11-08 more standard Resources.provide_parse_files: avoid duplicate markup reports;
20 months ago wenzelm 2018-09-24 tuned signature: prefer value-oriented pretty-printing;
20 months ago wenzelm 2018-09-24 tuned signature: prefer value-oriented pretty-printing;
21 months ago wenzelm 2018-09-02 no reset_proof for notepad: begin/end structure takes precedence over goal/proof structure;
21 months ago wenzelm 2018-08-28 tuned signature;
21 months ago wenzelm 2018-08-28 clarified ML_environment: ML_write_global requires "Isabelle";
21 months ago wenzelm 2018-08-27 clarified environment: allow "read>write" specification;
21 months ago wenzelm 2018-08-27 support named ML environments, notably "Isabelle", "SML"; more uniform options ML_read_global, ML_write_global; clarified bootstrap environment;
21 months ago wenzelm 2018-08-26 clarified signature;
23 months ago wenzelm 2018-06-26 clarified default tag;
23 months ago wenzelm 2018-06-21 clarified signature;
2018-05-25 wenzelm 2018-05-25 added command 'ML_export';
2018-03-06 ballarin 2018-03-06 Drop rewrite rule arguments of sublocale and interpretation implementations.
2018-03-04 ballarin 2018-03-04 Drop rewrites after defines in interpretations.
2018-03-02 ballarin 2018-03-02 Proper rewrite morphisms in locale instances.
2018-02-25 wenzelm 2018-02-25 tuned;
2018-01-16 ballarin 2018-01-16 Experimental support for rewrite morphisms in locale instances.
2018-01-16 wenzelm 2018-01-16 discontinued old form of marginal comments;
2018-01-09 wenzelm 2018-01-09 clarified modules;
2017-12-28 wenzelm 2017-12-28 prefer existing Resources.check_path;
2017-12-28 wenzelm 2017-12-28 added command 'bibtex_file' (for PIDE interaction only);
2017-12-22 wenzelm 2017-12-22 discontinued 'display_drafts' command;
2017-12-06 wenzelm 2017-12-06 prefer control symbol antiquotations;
2017-12-03 wenzelm 2017-12-03 discontinued old 'def' command;
2017-11-29 wenzelm 2017-11-29 clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform;
2017-11-08 wenzelm 2017-11-08 formal dependency on "poly" executable;
2017-11-05 wenzelm 2017-11-05 more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
2017-10-02 wenzelm 2017-10-02 added command 'external_file';
2017-07-02 haftmann 2017-07-02 proper concept of code declaration wrt. atomicity and Isar declarations
2017-07-03 wenzelm 2017-07-03 added command 'alias' and 'type_alias';
2017-06-26 wenzelm 2017-06-26 clarified indentation;
2016-12-28 wenzelm 2016-12-28 more uniform treatment of "bad" like other messages (with serial number);
2016-12-18 wenzelm 2016-12-18 tuned;
2016-09-14 wenzelm 2016-09-14 discontinued global etc/abbrevs;
2016-09-06 wenzelm 2016-09-06 strictly sequential abbrevs;
2016-08-02 wenzelm 2016-08-02 support 'abbrevs' within theory header; simplified 'keywords': no abbreviations here;
2016-07-16 wenzelm 2016-07-16 information about proof outline with cases (sendback);
2016-07-15 wenzelm 2016-07-15 singleton result for 'proof' command (without backtracking), e.g. relevant for well-defined output;
2016-07-11 wenzelm 2016-07-11 clarified indentation;
2016-07-11 wenzelm 2016-07-11 explicit kind "before_command"; tuned signature;
2016-07-11 wenzelm 2016-07-11 more indentation for quasi_command keywords;
2016-06-23 wenzelm 2016-06-23 tuned signature;