2010-04-25 ago modernized naming conventions of main Isar proof elements;
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-07 ago modernized structure Object_Logic;
2009-11-25 ago normalized uncurry take/drop
2009-11-24 ago curried take/drop
2009-11-02 ago modernized structure Proof_Display;
2009-11-02 ago modernized structure AutoBind;
2009-11-01 ago modernized structure Context_Rules;
2009-11-01 ago modernized structure Rule_Cases;
2009-10-17 ago indicate CRITICAL nature of various setmp combinators;
2009-09-30 ago eliminated dead code;
2009-07-26 ago Variable.focus: named parameters;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-06-24 ago renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
2009-03-28 ago renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 ago replaced add_binds(_i) by bind_terms -- internal version only;
2009-03-19 ago use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-03 ago renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
2009-03-03 ago Thm.binding;
2009-01-21 ago binding is alias for Binding.T
2009-01-07 ago qed/after_qed: singleton result;
2008-12-05 ago Name.name_of -> Binding.base_name
2008-12-04 ago cleaned up binding module and related code
2008-09-02 ago type Attrib.binding abbreviates Name.binding without attributes;
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2007-10-09 ago generic Syntax.pretty/string_of operations;
2007-04-03 ago renamed Variable.import to import_thms (avoid clash with Alice keywords);
2006-12-06 ago export: added explicit term operation;
2006-11-30 ago qualified MetaSimplifier.norm_hhf(_protect);
2006-11-07 ago moved statement to specification.ML;
2006-09-30 ago statement: Variable.fix_frees;
2006-08-02 ago added tactical result;
2006-07-27 ago moved basic assumption operations from structure ProofContext to Assumption;
2006-07-26 ago Variable.import(T): result includes fixed types/terms;
2006-07-25 ago added find_free (from term.ML);
2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2006-07-04 ago guess: proper context for polymorphic parameters;
2006-07-03 ago obtain_export: Thm.generalize;
2006-06-17 ago Term.internal;
2006-06-15 ago ProofContext: moved variable operations to struct Variable;
2006-06-11 ago fixes: include mixfix syntax;
2006-06-05 ago guess: more careful about local polymorphism;
2006-05-07 ago removed 'concl is' patterns;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-03-21 ago subtract (op =);
2006-02-02 ago Proof.refine_insert;
2006-02-02 ago obtain(_i): optional name for 'that';
2006-01-31 ago tuned comments;
2006-01-24 ago ProofContext.inferred_param;
2006-01-21 ago simplified type attribute;
2006-01-15 ago guess: used fixed inferred_type of vars;
2006-01-14 ago sane ERROR handling;
2006-01-13 ago uniform handling of fixes;
2006-01-10 ago generic attributes;
2005-11-16 ago Term.betapplys;
2005-11-10 ago guess: Seq.hd;
2005-11-08 ago simplified after_qed;
2005-10-28 ago renamed Goal constant to prop, more general protect/unprotect interfaces;