doc-src/IsarRef/pure.tex
2003-12-10 ballarin 2003-12-10 Isar: where attribute supports instantiation of type vars.
2003-09-30 ballarin 2003-09-30 Improvements wrt rule_tac.
2003-08-29 ballarin 2003-08-29 Method rule_tac understands Isar contexts: documentation.
2003-02-25 berghofe 2003-02-25 Documented prf / full_prf commands and antiquotations.
2002-08-27 wenzelm 2002-08-27 thms_containing: allow "_" in specification;
2002-07-02 wenzelm 2002-07-02 thms_containing: optional limit argument;
2002-07-02 wenzelm 2002-07-02 update thms_containing;
2002-03-08 wenzelm 2002-03-08 tuned;
2002-03-07 wenzelm 2002-03-07 tuned;
2002-03-07 wenzelm 2002-03-07 tuned;
2002-03-05 wenzelm 2002-03-05 more stuff;
2002-03-04 wenzelm 2002-03-04 tuned;
2002-02-28 wenzelm 2002-02-28 contexts, locales, sym(metric);
2002-02-27 wenzelm 2002-02-27 'using' command;
2002-02-12 wenzelm 2002-02-12 tuned;
2002-01-03 wenzelm 2002-01-03 next round of updates;
2002-01-02 wenzelm 2002-01-02 first stage of major update;
2001-09-04 wenzelm 2001-09-04 renamed "antecedent" case to "rule_context";
2001-02-12 wenzelm 2001-02-12 \<subseteq> syntax for classes/classrel/axclass/instance;
2001-02-01 wenzelm 2001-02-01 thms_containing: term args;
2001-01-16 wenzelm 2001-01-16 more method_setup examples;
2001-01-10 wenzelm 2001-01-10 tuned;
2000-12-16 wenzelm 2000-12-16 'def': equiv;
2000-12-11 wenzelm 2000-12-11 alternative syntax for "translations": harpoons;
2000-12-04 wenzelm 2000-12-04 diagnostic commands: comment;
2000-11-30 wenzelm 2000-11-30 schematic goals;
2000-10-15 wenzelm 2000-10-15 tuned;
2000-10-06 wenzelm 2000-10-06 tuned;
2000-09-12 wenzelm 2000-09-12 renamed "delrule" to "rule del";
2000-08-29 wenzelm 2000-08-29 'syntax': improved mode spec; 'pr': prems limit;
2000-08-28 wenzelm 2000-08-28 proper setup of iman.sty/extra.sty/ttbox.sty;
2000-08-14 wenzelm 2000-08-14 added 'declare' command; moved tactic emulations; tuned; renamed "res_inst_tac' etc. to 'rule_tac' etc.; tuned;
2000-07-30 wenzelm 2000-07-30 'def': no constraint on variable;
2000-07-13 wenzelm 2000-07-13 defs: (overloaded) option;
2000-07-06 wenzelm 2000-07-06 allow comment in more commands;
2000-07-04 wenzelm 2000-07-04 added "nothing" (empty list of theorems);
2000-07-01 wenzelm 2000-07-01 removed "help";
2000-06-29 wenzelm 2000-06-29 facts: support multiple lists of arguments; method_setup command;
2000-06-03 wenzelm 2000-06-03 'next', '{', '}': comment;
2000-05-31 wenzelm 2000-05-31 tuned tactic emulation;
2000-05-28 wenzelm 2000-05-28 case 'antecedent';
2000-05-24 wenzelm 2000-05-24 tuned;
2000-05-24 wenzelm 2000-05-24 "done" command;
2000-05-21 wenzelm 2000-05-21 replaced {{ }} by { };
2000-05-18 wenzelm 2000-05-18 'pr' now prints actual proof states only;
2000-05-18 wenzelm 2000-05-18 'apply' consumes facts;
2000-04-17 wenzelm 2000-04-17 'global' / 'local': comment; added 'hide';
2000-04-12 wenzelm 2000-04-12 tuned;
2000-04-12 wenzelm 2000-04-12 'insts' syntax; 'insert' method;
2000-04-10 wenzelm 2000-04-10 improved document preparation;
2000-04-07 wenzelm 2000-04-07 added 'ML_command'; 'apply' etc.: comments;
2000-04-04 wenzelm 2000-04-04 'let': replaced 'as' by 'and';
2000-03-31 wenzelm 2000-03-31 fixed goal syntax;
2000-03-30 wenzelm 2000-03-30 support Hindley-Milner polymorphisms in results and bindings;
2000-03-21 wenzelm 2000-03-21 tuned;
2000-03-20 wenzelm 2000-03-20 res_inst_tac etc.; subgoal_tac;
2000-03-18 wenzelm 2000-03-18 pure methods / atts moved here; tactic emulation moved here; oops moved here; history commands; tuned;
2000-03-17 wenzelm 2000-03-17 fixed theory, context typing; defer, prefer; tuned;
2000-03-16 wenzelm 2000-03-16 moved "cases" to generic.tex; improved diagnostic commands; history commands; tuned;
2000-03-14 wenzelm 2000-03-14 tuned 'case';