doc-src/IsarRef/generic.tex
2006-12-09 wenzelm 2006-12-09 added print_abbrevs;
2006-11-30 wenzelm 2006-11-30 simplified syntax for 'definition', 'abbreviation';
2006-11-17 wenzelm 2006-11-17 'notation': more robust 'and' list;
2006-11-11 wenzelm 2006-11-11 updated local theory targets; added 'context' as local theory switch; tuned;
2006-11-07 wenzelm 2006-11-07 'const_syntax' command: allow fixed variables, renamed to 'notation';
2006-10-20 haftmann 2006-10-20 small refinements
2006-09-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary';
2006-09-08 haftmann 2006-09-08 changed order of type classes and axclasses
2006-09-04 ballarin 2006-09-04 Documented methods intro_locales and unfold_locales.
2006-09-04 haftmann 2006-09-04 some corrections in class section
2006-08-14 haftmann 2006-08-14 added passage on class package
2006-07-14 wenzelm 2006-07-14 simp method: depth_limit;
2006-06-06 haftmann 2006-06-06 fixed typo
2006-05-16 wenzelm 2006-05-16 const_syntax;
2006-04-09 wenzelm 2006-04-09 unfold(ed): not necessrily meta equations;
2006-04-08 wenzelm 2006-04-08 refined 'abbreviation';
2006-02-27 ballarin 2006-02-27 Typo.
2006-02-16 wenzelm 2006-02-16 derived specifications: definition, abbreviation, axiomatization;
2006-02-02 wenzelm 2006-02-02 'obtain': optional case name;
2006-01-30 wenzelm 2006-01-30 'fixes': support plain vars; classical attributes: optional weight -- ignored by automated tools;
2005-12-31 wenzelm 2005-12-31 removed classical elim_format;
2005-12-23 wenzelm 2005-12-23 induct etc.: admit multiple rules;
2005-11-23 wenzelm 2005-11-23 added case_conclusion attribute; added coinduct method/attribute; induct method: definsts/fixing/taking; tuned;
2005-10-15 wenzelm 2005-10-15 added guess;
2005-09-06 wenzelm 2005-09-06 axclass: name space prefix is now "c_class" instead of just "c";
2005-09-02 ballarin 2005-09-02 print_locale omits facts by default
2005-08-24 ballarin 2005-08-24 Printing of interpretations: option to show witness theorems;
2005-08-10 ballarin 2005-08-10 New command: interpretation in locales.
2005-06-01 ballarin 2005-06-01 Locales: new element constrains, parameter renaming with syntax, experimental command instantiate withdrawn.
2005-05-27 ballarin 2005-05-27 Locale expressions: rename with optional mixfix syntax.
2005-05-19 nipkow 2005-05-19 subst again
2005-05-18 nipkow 2005-05-18 documented new subst
2005-04-25 ballarin 2005-04-25 Subsumption of locale interpretations.
2005-04-18 ballarin 2005-04-18 Interpretation supports statically scoped attributes; documentation.
2004-04-16 wenzelm 2004-04-16 'instance' and intro_classes now handle general sorts;
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.
2002-10-02 nipkow 2002-10-02 *** empty log message ***
2002-10-01 berghofe 2002-10-01 Documented new "asm_lr" option for simp.
2002-07-26 wenzelm 2002-07-26 support for split assumptions in cases (hyps vs. prems);
2002-07-24 wenzelm 2002-07-24 locales: predicate defs;
2002-03-08 wenzelm 2002-03-08 tuned;
2002-03-07 wenzelm 2002-03-07 tuned;
2002-03-07 wenzelm 2002-03-07 *** empty log message ***
2002-03-07 wenzelm 2002-03-07 tuned;
2002-03-07 wenzelm 2002-03-07 tuned;
2002-03-06 wenzelm 2002-03-06 some more stuff; 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 tuned;
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-10-04 wenzelm 2001-10-04 induct/cases made generic, removed simplified/stripped options;
2001-08-07 oheimb 2001-08-07 removed the warning from [iff]
2001-07-23 oheimb 2001-07-23 slight improvement for iff attribute
2001-05-31 oheimb 2001-05-31 corrected entry for iff attribute
2001-05-30 oheimb 2001-05-30 extended doc for iff attribute
2001-02-15 wenzelm 2001-02-15 index mod syntax;