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