src/Pure/assumption.ML
Tue, 06 Jun 2023 15:12:40 +0200 wenzelm proper trim_context / transfer, e.g. for Specification.definition;
Tue, 06 Jun 2023 14:19:53 +0200 wenzelm tuned;
Tue, 06 Jun 2023 11:07:49 +0200 wenzelm minor performance tuning: avoid append to end-of-list;
Sat, 20 May 2023 17:42:01 +0200 wenzelm tuned signature;
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);
Tue, 16 May 2023 14:30:32 +0200 wenzelm support for context within morphism (for background theory);
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);
Thu, 28 Nov 2019 18:13:23 +0100 wenzelm more structural integrity;
Thu, 19 Sep 2019 16:38:05 +0200 wenzelm explicit check of assumption prefix;
Mon, 03 Jun 2019 23:58:20 +0200 wenzelm more structural integrity;
Sun, 25 Feb 2018 15:44:46 +0100 wenzelm eliminated ASCII syntax from Pure bootstrap;
Fri, 19 Dec 2014 12:36:50 +0100 wenzelm tuned;
Fri, 10 Jan 2014 21:37:28 +0100 wenzelm more elementary management of declared hyps, below structure Assumption;
Tue, 31 Dec 2013 14:29:16 +0100 wenzelm proper context for norm_hhf and derived operations;
Fri, 13 Dec 2013 20:20:15 +0100 wenzelm maintain morphism names for diagnostic purposes;
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;
Sat, 31 Mar 2012 15:21:35 +0200 wenzelm tuned comment;
Wed, 15 Feb 2012 21:08:27 +0100 wenzelm discontinued obsolete "prems" fact;
Sun, 27 Nov 2011 21:53:38 +0100 wenzelm tuned;
Fri, 28 Oct 2011 15:38:41 +0200 wenzelm slightly more explicit/syntactic modelling of morphisms;
Fri, 14 Jan 2011 16:01:29 +0100 wenzelm global "prems" is legacy feature;
Fri, 17 Dec 2010 17:08:56 +0100 wenzelm renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
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;
Thu, 11 Mar 2010 23:07:12 +0100 wenzelm tuned signature;
Wed, 25 Nov 2009 09:13:46 +0100 haftmann normalized uncurry take/drop
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Thu, 12 Mar 2009 16:13:14 +0100 wenzelm tuned;
Thu, 12 Mar 2009 15:53:14 +0100 wenzelm renamed assms_of to all_assms_of, and prems_of to all_prems_of;
Wed, 21 Jan 2009 22:26:49 +0100 wenzelm eliminated obsolete var morphism;
Wed, 21 Jan 2009 16:47:04 +0100 haftmann binding replaces bstring
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
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
Tue, 25 Mar 2008 19:39:58 +0100 wenzelm setup for dynamic "prems" (legacy);
Mon, 07 May 2007 00:49:59 +0200 wenzelm simplified DataFun interfaces;
Wed, 06 Dec 2006 21:18:56 +0100 wenzelm export: added explicit term operation;
Thu, 30 Nov 2006 14:17:29 +0100 wenzelm qualified MetaSimplifier.norm_hhf(_protect);
Wed, 29 Nov 2006 04:11:10 +0100 wenzelm assms_of: cterm;
Fri, 24 Nov 2006 22:05:13 +0100 wenzelm added export_morphism;
Wed, 02 Aug 2006 22:26:50 +0200 wenzelm simplified export: no Seq.seq;
Thu, 27 Jul 2006 13:42:59 +0200 wenzelm Local assumptions, parameterized by export rules.
less more (0) tip