src/Pure/simplifier.ML
2009-03-07 wenzelm 2009-03-07 renamed rep_ss to MetaSimplifier.internal_ss;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-12-05 haftmann 2008-12-05 dropped NameSpace.declare_base
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-11-20 haftmann 2008-11-20 dropped legacy naming code
2008-11-14 haftmann 2008-11-14 namify and name_decl combinators
2008-11-13 haftmann 2008-11-13 consider prefixes for name bindings of simprocs (a first approximation)
2008-09-02 wenzelm 2008-09-02 name/var morphism operates on Name.binding;
2008-06-24 wenzelm 2008-06-24 ML_Antiquote.value;
2008-05-29 wenzelm 2008-05-29 proper context for attribute simplified;
2008-04-15 wenzelm 2008-04-15 Thm.forall_elim_var(s);
2008-03-29 wenzelm 2008-03-29 purely functional setup of claset/simpset/clasimpset; tuned signature;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-27 wenzelm 2008-03-27 renamed ML_Context.the_context to ML_Context.the_global_context;
2007-09-01 wenzelm 2007-09-01 replaced ProofContext.read_term/prop by general Syntax.read_term/prop; replaced ProofContext.cert_term/prop by general Syntax.check_term/prop (which also includes type-inference);
2007-08-02 wenzelm 2007-08-02 turned simp_depth_limit into configuration option;
2007-07-28 wenzelm 2007-07-28 added attribute "simproc"; marked some CRITICAL sections; tuned;
2007-07-08 wenzelm 2007-07-08 replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-07-05 wenzelm 2007-07-05 tuned;
2007-07-03 wenzelm 2007-07-03 moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
2007-05-24 haftmann 2007-05-24 tuned Pure/General/name_space.ML
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-23 wenzelm 2007-04-23 def_simproc(_i): proper ProofContext.read/cert_terms;
2007-04-16 haftmann 2007-04-16 canonical merge operations
2007-04-15 wenzelm 2007-04-15 removed obsolete TypeInfer.logicT -- use dummyT;
2007-02-28 wenzelm 2007-02-28 exported get_ss, map_ss;
2007-02-04 wenzelm 2007-02-04 def_simproc(_i): tuned interface; tuned simprocs environment;
2007-01-29 wenzelm 2007-01-29 added get_simproc, @{simproc};
2007-01-28 wenzelm 2007-01-28 added def_simproc(_i) -- define named simprocs; tuned;
2007-01-20 wenzelm 2007-01-20 added @{simpset};
2007-01-19 wenzelm 2007-01-19 moved ML context stuff to from Context to ML_Context;
2006-12-07 wenzelm 2006-12-07 reorganized structure Tactic vs. MetaSimplifier;
2006-12-07 wenzelm 2006-12-07 reorganized structure Goal vs. Tactic;
2006-11-10 haftmann 2006-11-10 introduces canonical AList functions for loop_tacs
2006-10-07 wenzelm 2006-10-07 tuned;
2006-02-10 wenzelm 2006-02-10 Args/Attrib syntax: Context.generic;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-14 wenzelm 2006-01-14 generic attributes;
2006-01-10 wenzelm 2006-01-10 Attrib.rule;
2005-10-28 wenzelm 2005-10-28 export cong_modifiers, simp_modifiers';
2005-10-21 wenzelm 2005-10-21 added simplification tactics and rules (from meta_simplifier.ML);
2005-10-18 wenzelm 2005-10-18 renamed set_context to context; data extend: reset context;
2005-10-17 wenzelm 2005-10-17 removed obsolete/experimental context components (superceded by Simplifier.the_context); more abstract change_simpset(_of); tuned;
2005-09-29 wenzelm 2005-09-29 export debug_bounds;
2005-08-02 wenzelm 2005-08-02 export clear_ss;
2005-08-01 wenzelm 2005-08-01 export MataSimplifier.inherit_bounds;
2005-07-13 wenzelm 2005-07-13 removed obsolete delta stuff;
2005-07-06 wenzelm 2005-07-06 multiple flags: prefer later ones;
2005-07-04 wenzelm 2005-07-04 made smlnj happy;
2005-07-04 wenzelm 2005-07-04 methods: added simp_flags argument, added "depth_limit" flag;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;
2005-05-22 wenzelm 2005-05-22 moved here from Provers; removed find_rewrites (superceded by find_theorems rewrite); outer syntax moved to Pure/Isar/isar_syn.ML;