src/Pure/Isar/expression.ML
Tue, 09 Oct 2012 20:23:58 +0200 wenzelm tuned;
Tue, 03 Apr 2012 20:24:00 +0200 wenzelm avoid duplicate PIDE markup;
Tue, 03 Apr 2012 18:22:14 +0200 wenzelm close context elements via Expression.cert/read_declaration;
Tue, 03 Apr 2012 11:21:17 +0200 wenzelm tuned;
Sun, 01 Apr 2012 19:07:32 +0200 wenzelm added Attrib.global_notes/local_notes/generic_notes convenience;
Wed, 21 Mar 2012 21:24:13 +0100 wenzelm tuned signature;
Wed, 14 Mar 2012 17:52:38 +0100 wenzelm source positions for locale and class expressions;
Tue, 13 Mar 2012 14:17:42 +0100 wenzelm refined 'interpret': reset facts ("this") and print_result, which merely consist of internal / protected statement;
Sat, 10 Mar 2012 20:02:15 +0100 wenzelm tuned;
Sat, 10 Mar 2012 17:07:10 +0100 wenzelm tuned;
Sat, 19 Nov 2011 16:16:33 +0100 wenzelm simplified Locale.add_thmss, after partial evaluation of attributes;
Sat, 19 Nov 2011 15:34:37 +0100 wenzelm misc tuning;
Sat, 19 Nov 2011 15:04:36 +0100 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;
Sat, 25 Jun 2011 12:19:54 +0200 ballarin While reading equations of an interpretation, already allow syntax provided by the interpretation base.
Wed, 27 Apr 2011 20:58:40 +0200 wenzelm tuned signature -- eliminated odd comment;
Wed, 27 Apr 2011 10:31:18 +0200 wenzelm more uniform Variable.add_frees/add_fixed etc.;
Thu, 21 Apr 2011 12:56:27 +0200 wenzelm discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
Sun, 17 Apr 2011 21:42:47 +0200 wenzelm added Binding.print convenience, which includes quote already;
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, 16 Apr 2011 15:25:25 +0200 wenzelm prefer local name spaces;
Sat, 16 Apr 2011 13:48:45 +0200 wenzelm Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
Sat, 16 Apr 2011 12:46:18 +0200 wenzelm tuned signature, disentangled dependencies;
Fri, 08 Apr 2011 16:34:14 +0200 wenzelm discontinued special treatment of structure Lexicon;
Sun, 16 Jan 2011 14:57:14 +0100 wenzelm added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
Thu, 06 Jan 2011 21:06:18 +0100 ballarin Diagnostic command to show locale dependencies.
Sat, 18 Dec 2010 18:43:13 +0100 ballarin Add mixins to sublocale command.
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;
Sun, 12 Sep 2010 19:04:02 +0200 wenzelm eliminated aliases of Type.constraint;
Thu, 26 Aug 2010 15:48:08 +0200 wenzelm renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
Thu, 26 Aug 2010 13:09:12 +0200 wenzelm renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
Thu, 12 Aug 2010 13:28:18 +0200 haftmann Named_Target.init: empty string represents theory target
Wed, 11 Aug 2010 14:45:38 +0200 haftmann renamed Theory_Target to the more appropriate Named_Target
Tue, 10 Aug 2010 22:26:23 +0200 ballarin Revert performance improvement of 8ed3a5fb4d25 since it breaks notes element declarations.
Thu, 05 Aug 2010 22:29:43 +0200 ballarin Remove duplicate locale activation code; performance improvement.
Sat, 31 Jul 2010 21:14:20 +0200 ballarin Interpretation in proofs supports mixins.
Sat, 31 Jul 2010 21:14:20 +0200 ballarin Make registrations generic data.
Fri, 04 Jun 2010 14:15:56 +0200 wenzelm tuned warning;
Thu, 27 May 2010 17:41:27 +0200 wenzelm renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
Wed, 05 May 2010 09:24:42 +0200 haftmann eq_morphism is always optional: avoid trivial morphism for empty list of equations
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;
Sat, 20 Mar 2010 17:33:11 +0100 wenzelm renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
Mon, 15 Mar 2010 18:59:16 +0100 wenzelm replaced type_syntax/term_syntax by uniform syntax_declaration;
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;
Sun, 21 Feb 2010 22:35:02 +0100 wenzelm slightly more abstract syntax mark/unmark operations;
Fri, 19 Feb 2010 20:41:34 +0100 wenzelm Thm.def_binding;
Thu, 18 Feb 2010 23:38:33 +0100 wenzelm locale: more precise treatment of naming vs. binding;
Tue, 16 Feb 2010 13:26:21 +0100 wenzelm comment;
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Fri, 13 Nov 2009 21:11:15 +0100 wenzelm modernized structure Local_Theory;
Fri, 13 Nov 2009 20:41:29 +0100 wenzelm eliminated slightly odd kind argument of LocalTheory.note(s);
Thu, 12 Nov 2009 22:29:54 +0100 wenzelm eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
Thu, 12 Nov 2009 22:02:11 +0100 wenzelm eliminated obsolete "internal" kind -- collapsed to unspecific "";
Tue, 10 Nov 2009 16:04:57 +0100 wenzelm modernized structure Theory_Target;
Fri, 30 Oct 2009 13:59:52 +0100 haftmann tuned variable names of bindings; conceal predicate constants
Thu, 29 Oct 2009 16:34:44 +0100 wenzelm eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
less more (0) -100 -60 tip