Thu, 03 Nov 2011 22:15:47 +0100 |
wenzelm |
tuned -- Variable.declare_term is already part of Variable.auto_fixes;
|
file |
diff |
annotate
|
Fri, 28 Oct 2011 22:17:30 +0200 |
wenzelm |
uniform Local_Theory.declaration with explicit params;
|
file |
diff |
annotate
|
Fri, 28 Oct 2011 17:15:52 +0200 |
wenzelm |
tuned signature -- refined terminology;
|
file |
diff |
annotate
|
Mon, 08 Aug 2011 17:23:15 +0200 |
wenzelm |
misc tuning -- eliminated old-fashioned rep_thm;
|
file |
diff |
annotate
|
Wed, 29 Jun 2011 21:34:16 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 29 Jun 2011 20:39:41 +0200 |
wenzelm |
simplified/unified Simplifier.mk_solver;
|
file |
diff |
annotate
|
Mon, 27 Jun 2011 16:53:31 +0200 |
wenzelm |
ML antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
Fri, 13 May 2011 23:58:40 +0200 |
wenzelm |
clarified map_simpset versus Simplifier.map_simpset_global;
|
file |
diff |
annotate
|
Fri, 13 May 2011 22:55:00 +0200 |
wenzelm |
proper Proof.context for classical tactics;
|
file |
diff |
annotate
|
Sat, 23 Apr 2011 17:02:12 +0200 |
wenzelm |
added Name_Space.check/get convenience;
|
file |
diff |
annotate
|
Sat, 23 Apr 2011 16:30:00 +0200 |
wenzelm |
clarified check_simproc (with report) vs. the_simproc;
|
file |
diff |
annotate
|
Sat, 23 Apr 2011 13:53:09 +0200 |
wenzelm |
proper binding/report of defined simprocs;
|
file |
diff |
annotate
|
Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 23:41:25 +0200 |
wenzelm |
PARALLEL_GOALS for method "simp_all";
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
Wed, 22 Dec 2010 20:08:40 +0100 |
haftmann |
tuned comment
|
file |
diff |
annotate
|
Fri, 17 Dec 2010 20:21:35 +0100 |
wenzelm |
more explicit references to structure Raw_Simplifier;
|
file |
diff |
annotate
|
Fri, 17 Dec 2010 17:08:56 +0100 |
wenzelm |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
|
file |
diff |
annotate
|
Fri, 17 Dec 2010 14:09:37 +0100 |
wenzelm |
clarified exports of structure Simplifier;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Tue, 15 Jun 2010 14:28:08 +0200 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Fri, 30 Apr 2010 23:33:42 +0200 |
wenzelm |
export Simplifier.with_context;
|
file |
diff |
annotate
|
Fri, 30 Apr 2010 17:18:29 +0200 |
wenzelm |
conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context;
|
file |
diff |
annotate
|
Thu, 29 Apr 2010 22:56:32 +0200 |
wenzelm |
proper context for mksimps etc. -- via simpset of the running Simplifier;
|
file |
diff |
annotate
|
Sat, 06 Mar 2010 15:39:16 +0100 |
wenzelm |
eliminated Args.bang_facts (legacy feature);
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
Tue, 10 Nov 2009 15:32:43 +0100 |
wenzelm |
define simprocs: do not apply target_morphism prematurely, this is already done in LocalTheory.declaration;
|
file |
diff |
annotate
|