src/Pure/Isar/isar_syn.ML
2005-03-24 ago Further work on interpretation commands. New command `interpret' for
2005-03-10 ago Registrations of global locale interpretations: improved, better naming.
2005-03-09 ago First version of global registration command.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2005-01-11 ago Added table of commands to be hidden in LaTeX output.
2004-10-11 ago Some changes to allow skipping of proof scripts.
2004-08-18 ago import -> imports
2004-08-16 ago new theory header syntax.
2004-08-12 ago Disallowed "includes" in locale declarations.
2004-06-21 ago Merged in license change from Isabelle2004
2004-06-15 ago path instead of string;
2004-06-13 ago added display_drafts and print_drafts commands;
2004-06-09 ago Syntax.default_mode;
2004-05-21 ago 'classrel' now allows multiple arguments;
2004-04-22 ago improved constdefs and translation functions;
2004-04-07 ago Locale instantiation: label parameter optional, new attribute paramter.
2004-04-02 ago Experimental command for instantiation of locales in proof contexts:
2003-10-09 ago Added support for making constants final, that is, ensuring that no
2003-02-03 ago Added "print_intros" command.
2002-08-02 ago fixed long statement: P.opt_thm_name;
2002-07-18 ago adapted locale syntax;
2002-07-16 ago locale: optional predicate name, or "open";
2002-07-02 ago thms_containing: optional limit argument;
2002-07-02 ago tuned msg;
2002-02-27 ago 'declare': and_list1;
2002-02-26 ago clarified general_statement syntax;
2002-02-26 ago tuned long_statement;
2002-02-25 ago updated markup commands;
2002-02-24 ago 'using' command;
2002-02-12 ago got rid of explicit marginal comments (now stripped earlier from input);
2002-01-15 ago allow empty locales;
2002-01-15 ago print_locale: allow full body specification;
2002-01-11 ago localized 'lemmas', 'theorems', 'declare';
2002-01-10 ago IsarThy.smart_multi_theorem;
2002-01-03 ago tuned msg;
2001-12-05 ago added 'print_rules' command;
2001-11-24 ago print_locale: expr;
2001-11-22 ago import locale expression;
2001-11-22 ago tuned;
2001-11-19 ago improved treatment of common result name;
2001-11-19 ago multi_theorem: common statement header (covers *all* results);
2001-11-11 ago "theorem" etc.: multiple statements;
2001-11-09 ago Commands prf and full_prf can now also be used to display proof term
2001-11-06 ago separate "in" locale vs. ad-hoc context;
2001-11-06 ago added 'locale', 'print_locales', 'print_locale';
2001-11-04 ago locale syntax;
2001-10-31 ago global statements: locale argument;
2001-10-22 ago improved source arrangement of obtain;
2001-10-16 ago support impromptu terminology of cases parameters;
2001-10-13 ago generic theorem kinds;
2001-10-04 ago added print_induct_rules;
2001-10-02 ago support non-oriented infix;
2001-08-31 ago Added functions for printing primitive proof terms.
2001-02-12 ago support \<subseteq> syntax in classes/classrel/axclass/instance;
2001-02-01 ago thms_containing: term args;
2001-01-18 ago show/thus: Toplevel.proof';
2000-12-16 ago 'def': \<equiv>;
2000-12-11 ago "translations": allow harpoons;
2000-12-04 ago dignostic commands: comment;