2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-04 wenzelm 2010-05-04 specification goal: eliminated redundant Thm.legacy_freezeT -- the goal is properly declared and should always produce fixed types in the result; specification result: replaced Thm.legacy_freezeT by Thm.unvarify_global -- the final result appears to be a closed term that is globally exported;
2010-05-03 wenzelm 2010-05-03 renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-25 wenzelm 2010-04-25 modernized naming conventions of main Isar proof elements;
2010-03-22 wenzelm 2010-03-22 eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;
2010-03-22 wenzelm 2010-03-22 replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-17 blanchet 2010-03-17 added support for "specification" and "ax_specification" constructs to Nitpick
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-27 wenzelm 2009-10-27 eliminated some old folds;
2009-10-17 wenzelm 2009-10-17 explicitly qualify Drule.standard;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"