2005-10-19 ago removed obsolete axclass_tac, add_inst_subclass_x, add_inst_arity_x;
2005-10-15 ago goal statements: accomodate before_qed argument;
2005-10-04 ago minor tweaks for Poplog/ML;
2005-09-29 ago Theory.add_finals_i;
2005-09-20 ago slight adaptions to library changes
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-13 ago tuned Isar interfaces;
2005-09-06 ago name space prefix is now "c_class" instead of just "c";
2005-09-01 ago curried_lookup/update;
2005-08-16 ago OuterKeyword;
2005-08-09 ago exported after_qed for arity proofs
2005-08-08 ago After_qed takes result argument.
2005-06-20 ago get_thm(s): Name;
2005-06-17 ago accomodate change of TheoryDataFun;
2005-06-11 ago refer to name spaces values instead of names;
2005-06-09 ago got rid of bclass, xclass;
2005-06-02 ago Theory.restore_naming;
2005-05-31 ago renamed cond_extern to extern;
2005-05-17 ago tuned;
2005-04-28 ago sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
2005-04-26 ago export intro_classes_tac;
2005-04-21 ago superceded by Pure.thy and CPure.thy;
2005-04-13 ago *** empty log message ***
2005-04-11 ago First release of interpretation commands.
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-24 ago Adapted to modified interface of PureThy.get_thm(s).
2004-06-21 ago Merged in license change from Isabelle2004
2004-06-01 ago removed obsolete sort 'logic';
2004-05-29 ago improved output;
2004-05-21 ago test_classrel/arity improve error reporting; tuned;
2004-05-01 ago improved Term.invent_names;
2004-04-16 ago 'instance' and intro_classes now handle general sorts;
2002-02-12 ago got rid of explicit marginal comments (now stripped earlier from input);
2002-01-10 ago simplified IsarThy.theorem_i;
2001-12-14 ago Term.invent_type_names;
2001-12-05 ago tuned;
2001-11-28 ago theory data: removed obsolete finish method;
2001-11-09 ago theory data: finish method;
2001-11-04 ago IsarThy.theorem_i (None, []);
2001-10-31 ago IsarThy.theorem_i: no locale;
2001-10-27 ago removed obsolete goal_subclass, goal_arity;
2001-10-18 ago sane internal interfaces for instance;
2001-10-13 ago IsarThy.theorem_i Drule.internalK;
2001-08-31 ago proper use of invent_names;
2001-08-31 ago tuned headers;
2001-05-31 ago invent_names
2001-02-12 ago support \<subseteq> syntax in classes/classrel/axclass/instance;
2000-11-21 ago Tactic.distinct_subgoals_tac moved to internal intro_classes_tac;
2000-11-18 ago default_intro_classes_tac: Tactic.distinct_subgoals_tac;
2000-11-13 ago tuned IsarThy.theorem_i;
2000-10-23 ago intro_classes by default;
2000-09-17 ago Display.pretty_thm_sg;
2000-05-23 ago eta-expanded to handle value polymorphism
2000-05-21 ago adapted to inner syntax of sorts;
2000-04-17 ago Pretty.chunks;
2000-04-14 ago intrn_arity: reject type abbreviations;
2000-04-05 ago HEADGOAL;