src/Doc/Isar_Ref/Spec.thy
16 months ago ballarin 2018-03-04 Drop rewrites after defines in interpretations.
16 months ago ballarin 2018-03-02 Proper rewrite morphisms in locale instances.
16 months ago wenzelm 2018-02-25 allow multiple entries of and_list (on both sides);
20 months ago wenzelm 2017-11-05 more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
20 months ago wenzelm 2017-10-25 more documentation;
21 months ago wenzelm 2017-10-02 added command 'external_file';
2017-07-03 wenzelm 2017-07-03 added command 'alias' and 'type_alias';
2017-04-17 wenzelm 2017-04-17 more uniform thy_deps (like class_deps), see also c48d536231fe;
2016-08-12 wenzelm 2016-08-12 more symbols;
2016-08-02 wenzelm 2016-08-02 clarified: 'imports' is de-facto mandatory;
2016-08-02 wenzelm 2016-08-02 support 'abbrevs' within theory header; simplified 'keywords': no abbreviations here;
2016-07-20 wenzelm 2016-07-20 clarified imports; tuned;
2016-06-11 wenzelm 2016-06-11 clarified syntax;
2016-06-10 wenzelm 2016-06-10 added command 'unbundle';
2016-06-10 wenzelm 2016-06-10 prefer hybrid 'bundle' command;
2016-06-09 wenzelm 2016-06-09 documentation;
2016-05-30 wenzelm 2016-05-30 allow 'for' fixes for multi_specs;
2016-05-29 wenzelm 2016-05-29 clarified check_open_spec / read_open_spec; allow 'for' fixes in 'abbreviation', 'definition';
2016-05-28 wenzelm 2016-05-28 clarified 'axiomatization';
2016-04-24 wenzelm 2016-04-24 added Isar command 'define';
2016-04-13 wenzelm 2016-04-13 eliminated "xname" and variants;
2016-04-13 wenzelm 2016-04-13 clarified syntax;
2016-04-07 wenzelm 2016-04-07 updated documentation;
2016-04-04 wenzelm 2016-04-04 more uniform ML file commands;
2016-01-13 wenzelm 2016-01-13 clarified example;
2016-01-13 wenzelm 2016-01-13 updated section on "Overloaded constant definitions";
2015-12-19 haftmann 2015-12-19 documentation on last state of the art concerning interpretation
2015-12-16 wenzelm 2015-12-16 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
2015-12-07 haftmann 2015-12-07 clarified terminology
2015-11-19 wenzelm 2015-11-19 tuned whitespace;
2015-11-14 haftmann 2015-11-14 represent both algebraic and local-theory views on locale interpretation in interfaces
2015-11-14 haftmann 2015-11-14 prefer "rewrites" and "defines" to note rewrite morphisms
2015-11-14 haftmann 2015-11-14 coalesce permanent_interpretation.ML with interpretation.ML
2015-11-13 wenzelm 2015-11-13 tuned;
2015-11-13 wenzelm 2015-11-13 tuned whitespace;
2015-11-13 wenzelm 2015-11-13 more uniform jEdit properties;
2015-11-09 wenzelm 2015-11-09 uniform mandatory qualifier for all locale expressions, including 'statespace' parent; removed obsolete '!' syntax;
2015-11-04 ballarin 2015-11-04 Keyword 'rewrites' identifies rewrite morphisms.
2015-11-04 ballarin 2015-11-04 Qualifiers in locale expressions default to mandatory regardless of the command.
2015-10-22 wenzelm 2015-10-22 more control symbols; tuned;
2015-10-21 wenzelm 2015-10-21 proper spaces around @{text};
2015-10-20 wenzelm 2015-10-20 isabelle update_cartouches -t;
2015-10-18 wenzelm 2015-10-18 more control symbols;
2015-10-17 wenzelm 2015-10-17 clarified nesting of paragraphs: indentation is taken into account more uniformly; tuned;
2015-10-16 wenzelm 2015-10-16 Markdown support in document text;
2015-10-14 wenzelm 2015-10-14 more symbols;
2015-10-12 wenzelm 2015-10-12 more symbols;
2015-10-12 wenzelm 2015-10-12 redundant due to \parindent 0pt;
2015-10-12 wenzelm 2015-10-12 more antiquotations;
2015-10-06 wenzelm 2015-10-06 fewer aliases for toplevel theorem statements;
2015-05-22 wenzelm 2015-05-22 tuned;
2015-04-16 wenzelm 2015-04-16 clarified thy_deps;
2015-04-16 wenzelm 2015-04-16 tuned signature;
2015-04-16 wenzelm 2015-04-16 misc tuning and clarification;
2015-04-09 wenzelm 2015-04-09 clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
2015-04-06 wenzelm 2015-04-06 support for 'restricted' modifier: only qualified accesses outside the local scope;
2015-04-04 wenzelm 2015-04-04 some explanation of 'private';
2015-04-03 wenzelm 2015-04-03 more uniform "verbose" option to print name space;
2015-04-01 wenzelm 2015-04-01 misc tuning -- keep name space more clean;
2015-04-01 wenzelm 2015-04-01 added command 'experiment';