src/Pure/simplifier.ML
Wed, 25 Aug 2010 18:36:22 +0200 wenzelm renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
Tue, 15 Jun 2010 14:28:08 +0200 haftmann tuned whitespace
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Fri, 30 Apr 2010 23:33:42 +0200 wenzelm export Simplifier.with_context;
Fri, 30 Apr 2010 17:18:29 +0200 wenzelm conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context;
Thu, 29 Apr 2010 22:56:32 +0200 wenzelm proper context for mksimps etc. -- via simpset of the running Simplifier;
Sat, 06 Mar 2010 15:39:16 +0100 wenzelm eliminated Args.bang_facts (legacy feature);
Fri, 19 Feb 2010 16:11:45 +0100 wenzelm renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
Fri, 13 Nov 2009 21:11:15 +0100 wenzelm modernized structure Local_Theory;
Tue, 10 Nov 2009 15:32:43 +0100 wenzelm define simprocs: do not apply target_morphism prematurely, this is already done in LocalTheory.declaration;
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Thu, 05 Nov 2009 22:08:47 +0100 wenzelm adapted LocalTheory.declaration;
Sun, 25 Oct 2009 19:19:35 +0100 wenzelm LocalTheory.naming_of;
Sun, 25 Oct 2009 13:04:06 +0100 wenzelm make SML/NJ happy;
Sat, 24 Oct 2009 20:54:08 +0200 wenzelm maintain explicit name space kind;
Sat, 24 Oct 2009 19:47:37 +0200 wenzelm renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
Sat, 24 Oct 2009 19:20:03 +0200 wenzelm eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
Wed, 30 Sep 2009 22:25:50 +0200 wenzelm eliminated dead code;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Thu, 23 Jul 2009 18:44:08 +0200 wenzelm renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Sat, 30 May 2009 12:53:11 +0200 wenzelm modernized method setup;
Fri, 20 Mar 2009 17:12:37 +0100 wenzelm Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
Sun, 15 Mar 2009 15:59:44 +0100 wenzelm simplified attribute setup;
Fri, 13 Mar 2009 21:25:15 +0100 wenzelm eliminated type Args.T;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Thu, 12 Mar 2009 11:10:02 +0100 wenzelm renamed NameSpace.bind to NameSpace.define;
Sun, 08 Mar 2009 12:15:58 +0100 wenzelm added dest_ss;
Sat, 07 Mar 2009 11:45:56 +0100 wenzelm renamed rep_ss to MetaSimplifier.internal_ss;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Fri, 05 Dec 2008 08:04:53 +0100 haftmann dropped NameSpace.declare_base
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Thu, 20 Nov 2008 19:06:02 +0100 haftmann dropped legacy naming code
Fri, 14 Nov 2008 08:50:10 +0100 haftmann namify and name_decl combinators
Thu, 13 Nov 2008 14:19:09 +0100 haftmann consider prefixes for name bindings of simprocs (a first approximation)
Tue, 02 Sep 2008 14:10:19 +0200 wenzelm name/var morphism operates on Name.binding;
Tue, 24 Jun 2008 19:43:14 +0200 wenzelm ML_Antiquote.value;
Thu, 29 May 2008 23:46:43 +0200 wenzelm proper context for attribute simplified;
Tue, 15 Apr 2008 16:12:05 +0200 wenzelm Thm.forall_elim_var(s);
Sat, 29 Mar 2008 22:55:57 +0100 wenzelm purely functional setup of claset/simpset/clasimpset;
Fri, 28 Mar 2008 20:02:04 +0100 wenzelm Context.>> : operate on Context.generic;
Thu, 27 Mar 2008 15:32:15 +0100 wenzelm eliminated delayed theory setup
Thu, 27 Mar 2008 14:41:10 +0100 wenzelm renamed ML_Context.the_context to ML_Context.the_global_context;
Sat, 01 Sep 2007 15:47:01 +0200 wenzelm replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
Thu, 02 Aug 2007 12:06:27 +0200 wenzelm turned simp_depth_limit into configuration option;
Sat, 28 Jul 2007 20:40:30 +0200 wenzelm added attribute "simproc";
Sun, 08 Jul 2007 19:51:58 +0200 wenzelm replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
Thu, 05 Jul 2007 20:01:35 +0200 wenzelm tuned;
Tue, 03 Jul 2007 17:17:11 +0200 wenzelm moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
Thu, 24 May 2007 08:37:37 +0200 haftmann tuned Pure/General/name_space.ML
Mon, 07 May 2007 00:49:59 +0200 wenzelm simplified DataFun interfaces;
Mon, 23 Apr 2007 20:44:09 +0200 wenzelm def_simproc(_i): proper ProofContext.read/cert_terms;
Mon, 16 Apr 2007 16:11:03 +0200 haftmann canonical merge operations
Sun, 15 Apr 2007 23:25:50 +0200 wenzelm removed obsolete TypeInfer.logicT -- use dummyT;
Wed, 28 Feb 2007 22:05:44 +0100 wenzelm exported get_ss, map_ss;
Sun, 04 Feb 2007 22:02:16 +0100 wenzelm def_simproc(_i): tuned interface;
Mon, 29 Jan 2007 19:58:14 +0100 wenzelm added get_simproc, @{simproc};
Sun, 28 Jan 2007 23:29:15 +0100 wenzelm added def_simproc(_i) -- define named simprocs;
Sat, 20 Jan 2007 14:09:17 +0100 wenzelm added @{simpset};
less more (0) -60 tip