src/Pure/simplifier.ML
Thu, 03 Nov 2011 22:15:47 +0100 wenzelm tuned -- Variable.declare_term is already part of Variable.auto_fixes;
Fri, 28 Oct 2011 22:17:30 +0200 wenzelm uniform Local_Theory.declaration with explicit params;
Fri, 28 Oct 2011 17:15:52 +0200 wenzelm tuned signature -- refined terminology;
Mon, 08 Aug 2011 17:23:15 +0200 wenzelm misc tuning -- eliminated old-fashioned rep_thm;
Wed, 29 Jun 2011 21:34:16 +0200 wenzelm tuned signature;
Wed, 29 Jun 2011 20:39:41 +0200 wenzelm simplified/unified Simplifier.mk_solver;
Mon, 27 Jun 2011 16:53:31 +0200 wenzelm ML antiquotations are managed as theory data, with proper name space and entity markup;
Fri, 13 May 2011 23:58:40 +0200 wenzelm clarified map_simpset versus Simplifier.map_simpset_global;
Fri, 13 May 2011 22:55:00 +0200 wenzelm proper Proof.context for classical tactics;
Sat, 23 Apr 2011 17:02:12 +0200 wenzelm added Name_Space.check/get convenience;
Sat, 23 Apr 2011 16:30:00 +0200 wenzelm clarified check_simproc (with report) vs. the_simproc;
Sat, 23 Apr 2011 13:53:09 +0200 wenzelm proper binding/report of defined simprocs;
Sun, 17 Apr 2011 19:54:04 +0200 wenzelm report Name_Space.declare/define, relatively to context;
Sat, 16 Apr 2011 23:41:25 +0200 wenzelm PARALLEL_GOALS for method "simp_all";
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Wed, 22 Dec 2010 20:08:40 +0100 haftmann tuned comment
Fri, 17 Dec 2010 20:21:35 +0100 wenzelm more explicit references to structure Raw_Simplifier;
Fri, 17 Dec 2010 17:08:56 +0100 wenzelm renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
Fri, 17 Dec 2010 14:09:37 +0100 wenzelm clarified exports of structure Simplifier;
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;
less more (0) -100 -50 -30 tip