src/Pure/simplifier.ML
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-06-15 haftmann 2010-06-15 tuned whitespace
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
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-30 wenzelm 2010-04-30 export Simplifier.with_context;
2010-04-30 wenzelm 2010-04-30 conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context; map_ss: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;
2010-04-29 wenzelm 2010-04-29 proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-03-06 wenzelm 2010-03-06 eliminated Args.bang_facts (legacy feature);
2010-02-19 wenzelm 2010-02-19 renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-10 wenzelm 2009-11-10 define simprocs: do not apply target_morphism prematurely, this is already done in LocalTheory.declaration;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-05 wenzelm 2009-11-05 adapted LocalTheory.declaration;
2009-10-25 wenzelm 2009-10-25 LocalTheory.naming_of;
2009-10-25 wenzelm 2009-10-25 make SML/NJ happy;
2009-10-24 wenzelm 2009-10-24 maintain explicit name space kind; export Name_Space.the_entry; tuned messages;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 wenzelm 2009-10-24 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-09-30 wenzelm 2009-09-30 eliminated dead code;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
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-05-30 wenzelm 2009-05-30 modernized method setup; tuned;
2009-03-20 wenzelm 2009-03-20 Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
2009-03-15 wenzelm 2009-03-15 simplified attribute setup;
2009-03-13 wenzelm 2009-03-13 eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-12 wenzelm 2009-03-12 renamed NameSpace.bind to NameSpace.define;
2009-03-08 wenzelm 2009-03-08 added dest_ss; proper context fo pretty_ss; tuned;
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};