| Sun, 29 Dec 2013 23:21:11 +0100 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 22:35:28 +0100 |
haftmann |
ephemeral interpretation also formally works on theory level
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
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:07:36 +0100 |
wenzelm |
more accurate goal context;
|
file |
diff |
annotate
|
| Fri, 16 Aug 2013 20:58:15 +0200 |
wenzelm |
more markup -- avoid old Locale.extern;
|
file |
diff |
annotate
|
| Sat, 27 Jul 2013 16:35:51 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| Thu, 30 May 2013 12:35:40 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| Sun, 26 May 2013 19:45:54 +0200 |
haftmann |
more specific structure for registration into theory and dependency onto locale
|
file |
diff |
annotate
|
| Sat, 25 May 2013 18:30:38 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:44:08 +0200 |
haftmann |
tuned structure
|
file |
diff |
annotate
|
| Wed, 22 May 2013 22:56:17 +0200 |
haftmann |
interpretation must always operate on the last element in a local theory stack, not on all elements: interpretated facts must disappear after pop from local theory stack, and transfer from last target is not enough
|
file |
diff |
annotate
|
| Wed, 22 May 2013 22:56:17 +0200 |
haftmann |
mark local theory as brittle also after interpretation inside locales;
|
file |
diff |
annotate
|
| Wed, 24 Apr 2013 11:32:54 +0200 |
haftmann |
avoid odd reinit after sublocale declaration
|
file |
diff |
annotate
|
| Tue, 23 Apr 2013 19:40:33 +0200 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| Tue, 23 Apr 2013 11:14:50 +0200 |
haftmann |
target-sensitive user-level commands interpretation and sublocale
|
file |
diff |
annotate
|
| Tue, 23 Apr 2013 11:14:50 +0200 |
haftmann |
ML interfaces for various kinds of interpretation
|
file |
diff |
annotate
|
| Tue, 23 Apr 2013 11:14:50 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sun, 21 Apr 2013 20:08:13 +0200 |
haftmann |
more sharing
|
file |
diff |
annotate
|
| Sun, 21 Apr 2013 16:29:40 +0200 |
haftmann |
interpretation: distinguish theories and proofs by explicit parameter rather than generic context;
|
file |
diff |
annotate
|
| Sun, 21 Apr 2013 10:41:18 +0200 |
haftmann |
dropped unusued identifier
|
file |
diff |
annotate
|
| Sun, 21 Apr 2013 10:41:18 +0200 |
haftmann |
avoid odd bifurcation with Attrib.local_notes vs. Locale.add_thmss -- n.b. note_eqns_dependency operates in a specific locale target
|
file |
diff |
annotate
|
| Sun, 21 Apr 2013 10:41:18 +0200 |
haftmann |
tuned for uniformity
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 22:36:03 +0100 |
ballarin |
Improvements to the print_dependencies command.
|
file |
diff |
annotate
|
| Thu, 11 Oct 2012 19:25:36 +0200 |
wenzelm |
refined aprop_tr' -- retain entity information by using type slot as adhoc marker;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2012 16:09:44 +0200 |
wenzelm |
refrain from quantifying outer fixes, to enable nesting of contexts like "context fixes x context assumes A x";
|
file |
diff |
annotate
|
| Thu, 11 Oct 2012 15:26:33 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2012 15:06:27 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2012 20:23:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 20:24:00 +0200 |
wenzelm |
avoid duplicate PIDE markup;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 18:22:14 +0200 |
wenzelm |
close context elements via Expression.cert/read_declaration;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 11:21:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 19:07:32 +0200 |
wenzelm |
added Attrib.global_notes/local_notes/generic_notes convenience;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 21:24:13 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 14 Mar 2012 17:52:38 +0100 |
wenzelm |
source positions for locale and class expressions;
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 14:17:42 +0100 |
wenzelm |
refined 'interpret': reset facts ("this") and print_result, which merely consist of internal / protected statement;
|
file |
diff |
annotate
|
| Sat, 10 Mar 2012 20:02:15 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 10 Mar 2012 17:07:10 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 16:16:33 +0100 |
wenzelm |
simplified Locale.add_thmss, after partial evaluation of attributes;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 15:34:37 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 15:04:36 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 17:15:52 +0200 |
wenzelm |
tuned signature -- refined terminology;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 15:38:41 +0200 |
wenzelm |
slightly more explicit/syntactic modelling of morphisms;
|
file |
diff |
annotate
|
| Sat, 25 Jun 2011 12:19:54 +0200 |
ballarin |
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 20:58:40 +0200 |
wenzelm |
tuned signature -- eliminated odd comment;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 10:31:18 +0200 |
wenzelm |
more uniform Variable.add_frees/add_fixed etc.;
|
file |
diff |
annotate
|
| Thu, 21 Apr 2011 12:56:27 +0200 |
wenzelm |
discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 21:42:47 +0200 |
wenzelm |
added Binding.print convenience, which includes quote already;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:25:25 +0200 |
wenzelm |
prefer local name spaces;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 12:46:18 +0200 |
wenzelm |
tuned signature, disentangled dependencies;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 06 Jan 2011 21:06:18 +0100 |
ballarin |
Diagnostic command to show locale dependencies.
|
file |
diff |
annotate
|
| Sat, 18 Dec 2010 18:43:13 +0100 |
ballarin |
Add mixins to sublocale command.
|
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
|
| Sun, 12 Sep 2010 19:04:02 +0200 |
wenzelm |
eliminated aliases of Type.constraint;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 13:28:18 +0200 |
haftmann |
Named_Target.init: empty string represents theory target
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 14:45:38 +0200 |
haftmann |
renamed Theory_Target to the more appropriate Named_Target
|
file |
diff |
annotate
|
| Tue, 10 Aug 2010 22:26:23 +0200 |
ballarin |
Revert performance improvement of 8ed3a5fb4d25 since it breaks notes element declarations.
|
file |
diff |
annotate
|
| Thu, 05 Aug 2010 22:29:43 +0200 |
ballarin |
Remove duplicate locale activation code; performance improvement.
|
file |
diff |
annotate
|
| Sat, 31 Jul 2010 21:14:20 +0200 |
ballarin |
Interpretation in proofs supports mixins.
|
file |
diff |
annotate
|
| Sat, 31 Jul 2010 21:14:20 +0200 |
ballarin |
Make registrations generic data.
|
file |
diff |
annotate
|
| Fri, 04 Jun 2010 14:15:56 +0200 |
wenzelm |
tuned warning;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Wed, 05 May 2010 09:24:42 +0200 |
haftmann |
eq_morphism is always optional: avoid trivial morphism for empty list of equations
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 15 Mar 2010 18:59:16 +0100 |
wenzelm |
replaced type_syntax/term_syntax by uniform syntax_declaration;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 11:57:16 +0100 |
wenzelm |
modernized structure Local_Defs;
|
file |
diff |
annotate
|
| Sun, 21 Feb 2010 22:35:02 +0100 |
wenzelm |
slightly more abstract syntax mark/unmark operations;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 20:41:34 +0100 |
wenzelm |
Thm.def_binding;
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 23:38:33 +0100 |
wenzelm |
locale: more precise treatment of naming vs. binding;
|
file |
diff |
annotate
|
| Tue, 16 Feb 2010 13:26:21 +0100 |
wenzelm |
comment;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 20:41:29 +0100 |
wenzelm |
eliminated slightly odd kind argument of LocalTheory.note(s);
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 22:29:54 +0100 |
wenzelm |
eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 22:02:11 +0100 |
wenzelm |
eliminated obsolete "internal" kind -- collapsed to unspecific "";
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 16:04:57 +0100 |
wenzelm |
modernized structure Theory_Target;
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 13:59:52 +0100 |
haftmann |
tuned variable names of bindings; conceal predicate constants
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 16:34:44 +0100 |
wenzelm |
eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 16:25:27 +0100 |
wenzelm |
conceal internal bindings;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 21:35:46 +0100 |
wenzelm |
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 10:15:31 +0200 |
haftmann |
removed old-style \ and \\ infixes
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 20:52:18 +0200 |
ballarin |
Merged.
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 20:37:33 +0200 |
ballarin |
Avoid administrative overhead for identity mixins.
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 11:33:32 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 07:40:25 +0200 |
ballarin |
Merged.
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 22:15:54 +0200 |
ballarin |
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
|
file |
diff |
annotate
|
| Sat, 19 Sep 2009 18:43:11 +0200 |
ballarin |
Explicit management of registration mixins.
|
file |
diff |
annotate
|
| Wed, 19 Aug 2009 19:35:46 +0200 |
ballarin |
Improved comments and api names.
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 22:24:57 +0200 |
wenzelm |
eliminated redundant parameters;
|
file |
diff |
annotate
|
| Thu, 03 Sep 2009 15:39:02 +0200 |
haftmann |
proper class syntax for sublocale class < expr
|
file |
diff |
annotate
|
| Wed, 15 Jul 2009 18:20:08 +0200 |
haftmann |
simplification of locale interfaces
|
file |
diff |
annotate
|
| Fri, 10 Jul 2009 07:59:44 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Fri, 10 Jul 2009 07:59:29 +0200 |
haftmann |
tuned locale interface
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:48:12 +0200 |
wenzelm |
renamed structure TermSubst to Term_Subst;
|
file |
diff |
annotate
|
| Mon, 30 Mar 2009 15:16:58 +0200 |
wenzelm |
prep_full_context_statement: explicit record of flags;
|
file |
diff |
annotate
|
| Sun, 29 Mar 2009 19:48:35 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sun, 29 Mar 2009 17:38:01 +0200 |
ballarin |
Merged.
|
file |
diff |
annotate
|
| Sun, 29 Mar 2009 17:22:17 +0200 |
ballarin |
Normalise equation only for morphism, not thm stored in theory.
|
file |
diff |
annotate
|
| Sun, 29 Mar 2009 19:41:04 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 29 Mar 2009 18:06:14 +0200 |
wenzelm |
simplified Element.activate(_i): singleton version;
|
file |
diff |
annotate
|
| Sun, 29 Mar 2009 17:47:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 29 Mar 2009 16:13:44 +0200 |
wenzelm |
unified binding prefix terminology;
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 20:25:23 +0100 |
wenzelm |
simplified Locale.activate operations, using generic context;
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 17:53:33 +0100 |
wenzelm |
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 17:21:49 +0100 |
wenzelm |
define_prefs: removed redundant Drule.gen_all, which is already part of the norm_hhf stage of Assumption.assume;
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 16:00:54 +0100 |
wenzelm |
simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 17:00:59 +0100 |
wenzelm |
register_locale: produce stamps at the spot where elements are registered;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 13:28:55 +0100 |
wenzelm |
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 13:18:42 +0100 |
wenzelm |
renamed sticky_prefix to mandatory_path;
|
file |
diff |
annotate
|