src/Pure/Isar/isar_syn.ML
2004-04-02 ballarin 2004-04-02 Experimental command for instantiation of locales in proof contexts: instantiate <label>: <loc>
2003-10-09 skalberg 2003-10-09 Added support for making constants final, that is, ensuring that no definition can be given later (useful for constants whose behaviour is fixed axiomatically rather than definitionally).
2003-02-03 berghofe 2003-02-03 Added "print_intros" command.
2002-08-02 wenzelm 2002-08-02 fixed long statement: P.opt_thm_name;
2002-07-18 wenzelm 2002-07-18 adapted locale syntax;
2002-07-16 wenzelm 2002-07-16 locale: optional predicate name, or "open";
2002-07-02 wenzelm 2002-07-02 thms_containing: optional limit argument;
2002-07-02 wenzelm 2002-07-02 tuned msg;
2002-02-27 wenzelm 2002-02-27 'declare': and_list1; 'obtain': updated;
2002-02-26 wenzelm 2002-02-26 clarified general_statement syntax;
2002-02-26 wenzelm 2002-02-26 tuned long_statement;
2002-02-25 wenzelm 2002-02-25 updated markup commands; clarified syntax of ``long'' statements: fixes/assumes/shows;
2002-02-24 wenzelm 2002-02-24 'using' command;
2002-02-12 wenzelm 2002-02-12 got rid of explicit marginal comments (now stripped earlier from input);
2002-01-15 wenzelm 2002-01-15 allow empty locales;
2002-01-15 wenzelm 2002-01-15 print_locale: allow full body specification;
2002-01-11 wenzelm 2002-01-11 localized 'lemmas', 'theorems', 'declare';
2002-01-10 wenzelm 2002-01-10 IsarThy.smart_multi_theorem;
2002-01-03 wenzelm 2002-01-03 tuned msg;
2001-12-05 wenzelm 2001-12-05 added 'print_rules' command;
2001-11-24 wenzelm 2001-11-24 print_locale: expr;
2001-11-22 wenzelm 2001-11-22 import locale expression;
2001-11-22 wenzelm 2001-11-22 tuned;
2001-11-19 wenzelm 2001-11-19 improved treatment of common result name;
2001-11-19 wenzelm 2001-11-19 multi_theorem: common statement header (covers *all* results);
2001-11-11 wenzelm 2001-11-11 "theorem" etc.: multiple statements;
2001-11-09 berghofe 2001-11-09 Commands prf and full_prf can now also be used to display proof term of current proof state.
2001-11-06 wenzelm 2001-11-06 separate "in" locale vs. ad-hoc context;
2001-11-06 wenzelm 2001-11-06 added 'locale', 'print_locales', 'print_locale';
2001-11-04 wenzelm 2001-11-04 locale syntax;
2001-10-31 wenzelm 2001-10-31 global statements: locale argument;
2001-10-22 wenzelm 2001-10-22 improved source arrangement of obtain;
2001-10-16 wenzelm 2001-10-16 support impromptu terminology of cases parameters;
2001-10-13 wenzelm 2001-10-13 generic theorem kinds;
2001-10-04 wenzelm 2001-10-04 added print_induct_rules;
2001-10-02 wenzelm 2001-10-02 support non-oriented infix;
2001-08-31 berghofe 2001-08-31 Added functions for printing primitive proof terms.
2001-02-12 wenzelm 2001-02-12 support \<subseteq> syntax in classes/classrel/axclass/instance;
2001-02-01 wenzelm 2001-02-01 thms_containing: term args;
2001-01-18 wenzelm 2001-01-18 show/thus: Toplevel.proof';
2000-12-16 wenzelm 2000-12-16 'def': \<equiv>;
2000-12-11 wenzelm 2000-12-11 "translations": allow harpoons;
2000-12-04 wenzelm 2000-12-04 dignostic commands: comment;
2000-11-13 wenzelm 2000-11-13 tuned statement args;
2000-09-15 wenzelm 2000-09-15 ML_command: no_timing;
2000-09-01 wenzelm 2000-09-01 'declare' made proper command;
2000-08-29 wenzelm 2000-08-29 pr: added prems limit;
2000-08-14 wenzelm 2000-08-14 added "declare" command;
2000-08-08 wenzelm 2000-08-08 prf_heading kind;
2000-07-30 wenzelm 2000-07-30 def: no constraint on var;
2000-07-27 wenzelm 2000-07-27 added thm_deps;
2000-07-13 wenzelm 2000-07-13 defs: (overloaded) option;
2000-07-06 wenzelm 2000-07-06 allow comment in more commands;
2000-07-01 wenzelm 2000-07-01 removed "help"; added "print_commands", "print_trans_rules", "print_antiquotations";
2000-06-29 wenzelm 2000-06-29 added method_setup; facts: handle multiple lists of arguments;
2000-06-25 wenzelm 2000-06-25 use ThyHeader.args; adapted OuterSyntax.markup_command;
2000-06-08 wenzelm 2000-06-08 prf_open/close;
2000-06-04 wenzelm 2000-06-04 opt_mixfix', opt_infix';
2000-06-03 wenzelm 2000-06-03 block commands: marginal comment;
2000-05-31 wenzelm 2000-05-31 Toplevel.no_timing;