| Tue, 06 Jun 2023 15:12:40 +0200 |
wenzelm |
proper trim_context / transfer, e.g. for Specification.definition;
|
file |
diff |
annotate
|
| Tue, 06 Jun 2023 14:19:53 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 06 Jun 2023 11:07:49 +0200 |
wenzelm |
minor performance tuning: avoid append to end-of-list;
|
file |
diff |
annotate
|
| Sat, 20 May 2023 17:42:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 20 May 2023 16:12:37 +0200 |
wenzelm |
more robust context: fail immediately via Morphism.the_theory, instead of rarely via Thm.theory_of_thm (for non-normal thm);
|
file |
diff |
annotate
|
| Tue, 16 May 2023 14:30:32 +0200 |
wenzelm |
support for context within morphism (for background theory);
|
file |
diff |
annotate
|
| Mon, 15 May 2023 14:13:58 +0200 |
wenzelm |
avoid capture of inner/outer context and thus reduce heaps sizes by 20..40% (see also dd04a8b654fc, e49bf4ebf330, 9c19e15c8548, 71467e35fc3c);
|
file |
diff |
annotate
|
| Thu, 28 Nov 2019 18:13:23 +0100 |
wenzelm |
more structural integrity;
|
file |
diff |
annotate
|
| Thu, 19 Sep 2019 16:38:05 +0200 |
wenzelm |
explicit check of assumption prefix;
|
file |
diff |
annotate
|
| Mon, 03 Jun 2019 23:58:20 +0200 |
wenzelm |
more structural integrity;
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 15:44:46 +0100 |
wenzelm |
eliminated ASCII syntax from Pure bootstrap;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 12:36:50 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 21:37:28 +0100 |
wenzelm |
more elementary management of declared hyps, below structure Assumption;
|
file |
diff |
annotate
|
| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|
| Fri, 13 Dec 2013 20:20:15 +0100 |
wenzelm |
maintain morphism names for diagnostic purposes;
|
file |
diff |
annotate
|
| Sat, 23 Nov 2013 17:15:44 +0100 |
wenzelm |
more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal -- NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
|
file |
diff |
annotate
|
| Sat, 31 Mar 2012 15:21:35 +0200 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 21:08:27 +0100 |
wenzelm |
discontinued obsolete "prems" fact;
|
file |
diff |
annotate
|
| Sun, 27 Nov 2011 21:53:38 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 15:38:41 +0200 |
wenzelm |
slightly more explicit/syntactic modelling of morphisms;
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 16:01:29 +0100 |
wenzelm |
global "prems" is legacy feature;
|
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
|
| Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 23:07:12 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 09:13:46 +0100 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 16:13:14 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 15:53:14 +0100 |
wenzelm |
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 22:26:49 +0100 |
wenzelm |
eliminated obsolete var morphism;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:04 +0100 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 20:02:04 +0100 |
wenzelm |
Context.>> : operate on Context.generic;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 15:32:15 +0100 |
wenzelm |
eliminated delayed theory setup
|
file |
diff |
annotate
|
| Tue, 25 Mar 2008 19:39:58 +0100 |
wenzelm |
setup for dynamic "prems" (legacy);
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2006 21:18:56 +0100 |
wenzelm |
export: added explicit term operation;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 14:17:29 +0100 |
wenzelm |
qualified MetaSimplifier.norm_hhf(_protect);
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 04:11:10 +0100 |
wenzelm |
assms_of: cterm;
|
file |
diff |
annotate
|
| Fri, 24 Nov 2006 22:05:13 +0100 |
wenzelm |
added export_morphism;
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:50 +0200 |
wenzelm |
simplified export: no Seq.seq;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 13:42:59 +0200 |
wenzelm |
Local assumptions, parameterized by export rules.
|
file |
diff |
annotate
|