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;
2005-10-21 ago improved check_result;
2005-10-18 ago tuned error msg;
2005-10-15 ago added 'guess', which derives the obtained context from the course of reasoning;
2005-09-13 ago tuned Isar proof elements;
2005-08-18 ago prepare attributes here;
2005-08-08 ago After_qed takes result argument.
2005-07-14 ago tuned;
2005-07-13 ago (intermediate commit)
2005-06-29 ago no Syntax.internal on thesis;
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-06-21 ago Merged in license change from Isabelle2004
2002-02-27 ago improved messages;
2001-12-06 ago Syntax.internal thesis;
2001-12-03 ago renamed rule_context.ML to context_rules.ML;
2001-11-29 ago RuleContext.intro_query_local;
2001-11-11 ago Proof.have_i: multiple statements;