src/Pure/Isar/object_logic.ML
Tue, 21 Sep 2021 12:35:38 +0200 wenzelm proper Sign.const_typargs via Theory.add_deps_const/Theory.const_dep;
Tue, 06 Aug 2019 16:15:22 +0200 wenzelm clarified context: proper transfer;
Sun, 21 Jul 2019 12:28:02 +0200 wenzelm tuned;
Tue, 26 Mar 2019 13:25:32 +0100 wenzelm export propositional status of consts;
Wed, 16 Dec 2015 16:31:36 +0100 wenzelm rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
Tue, 22 Sep 2015 22:38:22 +0200 wenzelm eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
Tue, 22 Sep 2015 14:32:23 +0200 wenzelm HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
Wed, 02 Sep 2015 21:54:00 +0200 wenzelm trim context for persistent storage;
Tue, 28 Jul 2015 20:59:39 +0200 wenzelm more explicit context;
Thu, 11 Jun 2015 10:03:54 +0200 wenzelm tuned;
Wed, 08 Apr 2015 19:39:08 +0200 wenzelm proper context for Object_Logic operations;
Sat, 07 Mar 2015 21:32:31 +0100 wenzelm clarified Drule.gen_all: observe context more carefully;
Fri, 21 Mar 2014 10:45:03 +0100 wenzelm tuned signature;
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Fri, 23 Aug 2013 20:35:50 +0200 wenzelm added Theory.setup convenience;
Thu, 30 May 2013 13:07:23 +0200 wenzelm tuned signature;
Sun, 06 Nov 2011 21:51:46 +0100 wenzelm more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
Sun, 17 Apr 2011 19:54:04 +0200 wenzelm report Name_Space.declare/define, relatively to context;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Sat, 15 Jan 2011 20:51:22 +0100 wenzelm clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
Mon, 10 Jan 2011 16:45:28 +0100 wenzelm added merge_options convenience;
Fri, 17 Dec 2010 17:08:56 +0100 wenzelm renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
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;
Sun, 07 Mar 2010 12:47:02 +0100 wenzelm separate structure Typedecl;
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Mon, 15 Feb 2010 17:17:51 +0100 wenzelm discontinued unnamed infix syntax;
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data;
Sat, 24 Oct 2009 18:55:47 +0200 wenzelm tuned message;
Sat, 07 Mar 2009 22:16:50 +0100 wenzelm more uniform handling of binding in targets and derived elements;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Thu, 16 Oct 2008 22:44:29 +0200 wenzelm Drule.norm_hhf_eqs;
Mon, 07 Apr 2008 21:25:18 +0200 wenzelm renamed iterated forall_conv to params_conv;
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
Wed, 28 Nov 2007 16:44:24 +0100 wenzelm added base_sort;
Sat, 13 Oct 2007 17:16:41 +0200 wenzelm replaced obsolete Theory.add_finals_i by Theory.add_deps;
Thu, 04 Oct 2007 20:29:24 +0200 wenzelm replaced literal 'a by Name.aT;
Thu, 04 Oct 2007 16:59:28 +0200 wenzelm Conv.forall_conv: proper context;
Sun, 29 Jul 2007 14:29:54 +0200 wenzelm renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
Thu, 05 Jul 2007 20:01:39 +0200 wenzelm tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
Thu, 05 Jul 2007 00:06:25 +0200 wenzelm avoid polymorphic equality;
Wed, 04 Jul 2007 16:49:34 +0200 wenzelm replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
Tue, 03 Jul 2007 17:17:15 +0200 wenzelm CONVERSION tactical;
Thu, 10 May 2007 00:39:45 +0200 wenzelm moved conversions to structure Conv;
Mon, 07 May 2007 00:49:59 +0200 wenzelm simplified DataFun interfaces;
Thu, 26 Apr 2007 12:00:05 +0200 wenzelm renamed some old names Theory.xxx to Sign.xxx;
Thu, 07 Dec 2006 23:16:55 +0100 wenzelm reorganized structure Tactic vs. MetaSimplifier;
Thu, 07 Dec 2006 00:42:04 +0100 wenzelm reorganized structure Goal vs. Tactic;
Mon, 09 Oct 2006 02:20:05 +0200 wenzelm attribute: Context.mapping;
Tue, 14 Mar 2006 16:29:38 +0100 wenzelm added is_elim (from Provers/classical.ML);
Mon, 06 Feb 2006 20:59:06 +0100 wenzelm tuned;
Sun, 29 Jan 2006 19:23:49 +0100 wenzelm moved treatment of object-logic equalities to local_defs.ML;
Sat, 28 Jan 2006 17:28:59 +0100 wenzelm removed unatomize;
Fri, 27 Jan 2006 19:03:13 +0100 wenzelm renamed reverse_atomize to unatomize;
Wed, 25 Jan 2006 00:21:41 +0100 wenzelm tuned atomize_cterm;
Sat, 21 Jan 2006 23:02:14 +0100 wenzelm simplified type attribute;
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Wed, 04 Jan 2006 00:52:45 +0100 wenzelm tuned;
less more (0) -60 tip