src/Pure/Isar/element.ML
Sat, 19 Nov 2011 13:02:50 +0100 wenzelm do not store vacuous theorem specifications -- relevant for frugal local theory content;
Mon, 07 Nov 2011 17:00:23 +0100 wenzelm tuned signature -- avoid spurious Thm.mixed_attribute;
Sat, 05 Nov 2011 20:40:30 +0100 wenzelm more uniform instT_subst vs. inst_subst: compare variable names only;
Sat, 05 Nov 2011 19:47:22 +0100 wenzelm some performance tuning via Term_Subst/Same.operation;
Sat, 05 Nov 2011 18:58:40 +0100 wenzelm pruned signature;
Thu, 03 Nov 2011 23:32:31 +0100 wenzelm tuned whitespace;
Sat, 29 Oct 2011 00:23:58 +0200 wenzelm tuned;
Fri, 28 Oct 2011 17:15:52 +0200 wenzelm tuned signature -- refined terminology;
Fri, 28 Oct 2011 15:38:41 +0200 wenzelm slightly more explicit/syntactic modelling of morphisms;
Mon, 08 Aug 2011 17:23:15 +0200 wenzelm misc tuning -- eliminated old-fashioned rep_thm;
Fri, 15 Jul 2011 16:51:01 +0200 wenzelm Element.activate: leave check of binding where actually applied to the context -- allow internal qualifications, or non-identifier fact names like "assumes *: A" (see also 1183951365de);
Fri, 15 Jul 2011 00:03:47 +0200 wenzelm do not check vacous bindings, which routinely occur in locale expressions and long theorem statements etc.;
Sat, 25 Jun 2011 17:17:49 +0200 wenzelm clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
Wed, 27 Apr 2011 21:50:04 +0200 wenzelm clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
Wed, 27 Apr 2011 20:58:40 +0200 wenzelm tuned signature -- eliminated odd comment;
Wed, 27 Apr 2011 17:58:45 +0200 wenzelm reorganized fixes as specialized (global) name space;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Sat, 16 Apr 2011 12:46:18 +0200 wenzelm tuned signature, disentangled dependencies;
Fri, 08 Apr 2011 14:20:57 +0200 wenzelm discontinued special treatment of structure Mixfix;
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, 03 Jan 2011 14:01:42 +0100 haftmann tuned whitespace
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;
Mon, 06 Sep 2010 22:58:06 +0200 wenzelm turned show_hyps and show_tags into proper configuration option;
Wed, 25 Aug 2010 15:12:49 +0200 wenzelm structure Thm: less pervasive names;
Sat, 31 Jul 2010 21:14:20 +0200 ballarin Interpretation in proofs supports mixins.
Wed, 05 May 2010 09:24:42 +0200 haftmann eq_morphism is always optional: avoid trivial morphism for empty list of equations
Sun, 25 Apr 2010 15:52:03 +0200 wenzelm modernized naming conventions of main Isar proof elements;
Sat, 13 Mar 2010 20:44:12 +0100 wenzelm removed unused Args.maxidx_values and Element.generalize_facts;
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Sun, 07 Mar 2010 11:57:16 +0100 wenzelm modernized structure Local_Defs;
Mon, 02 Nov 2009 20:57:48 +0100 wenzelm modernized structure Proof_Display;
Sun, 26 Jul 2009 13:12:54 +0200 wenzelm Variable.focus: named parameters;
Sat, 25 Jul 2009 18:04:15 +0200 wenzelm Method.Basic: no position;
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Wed, 24 Jun 2009 21:28:02 +0200 wenzelm renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
Sun, 29 Mar 2009 18:06:14 +0200 wenzelm simplified Element.activate(_i): singleton version;
Sun, 29 Mar 2009 17:47:50 +0200 wenzelm added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
Sat, 28 Mar 2009 17:53:33 +0100 wenzelm renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
Sat, 28 Mar 2009 17:21:11 +0100 wenzelm renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
Thu, 19 Mar 2009 13:28:55 +0100 wenzelm use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Wed, 11 Mar 2009 16:36:27 +0100 wenzelm eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
Wed, 11 Mar 2009 15:38:25 +0100 wenzelm Thm.def_binding_optional;
Sun, 08 Mar 2009 17:26:14 +0100 wenzelm moved basic algebra of long names from structure NameSpace to Long_Name;
Thu, 05 Mar 2009 12:08:00 +0100 wenzelm renamed NameSpace.base to NameSpace.base_name;
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Tue, 03 Mar 2009 18:32:01 +0100 wenzelm renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
Tue, 03 Mar 2009 15:09:09 +0100 wenzelm Binding.str_of;
Tue, 03 Mar 2009 14:07:43 +0100 wenzelm Thm.binding;
Wed, 21 Jan 2009 22:26:48 +0100 wenzelm eliminated obsolete var morphism;
Wed, 21 Jan 2009 16:47:03 +0100 haftmann refined witness algebra
Sat, 17 Jan 2009 08:29:40 +0100 haftmann explicit equation morphism
Tue, 16 Dec 2008 20:18:46 +0100 ballarin Transfer morphism with theory closure.
Tue, 16 Dec 2008 15:08:08 +0100 ballarin Finer-grained activation so that facts from earlier elements are available.
Tue, 16 Dec 2008 12:08:10 +0100 ballarin Use correct mode when parsing elements and conclusion.
Fri, 05 Dec 2008 18:43:42 +0100 haftmann Name.name_of -> Binding.base_name
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Tue, 25 Nov 2008 18:07:33 +0100 ballarin Use standard export function.
less more (0) -100 -60 tip