| Wed, 03 Oct 2012 16:42:36 +0200 |
wenzelm |
use explicit Type.strip_sorts_dummy to suppress sort constraints in output;
|
file |
diff |
annotate
|
| Sun, 17 Jun 2012 20:38:12 +0200 |
haftmann |
clarifying comment
|
file |
diff |
annotate
|
| Mon, 18 Jun 2012 15:48:43 +0200 |
haftmann |
class target handles additional non-class term parameters appropriately
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 13:47:15 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 10:59:20 +0200 |
wenzelm |
more uniform theory_abbrev with const_declaration;
|
file |
diff |
annotate
|
| Mon, 02 Apr 2012 21:49:27 +0200 |
wenzelm |
clarified standard_declaration vs. theory_declaration;
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 20:36:33 +0200 |
wenzelm |
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 14:29:22 +0200 |
wenzelm |
Local_Theory.map_contexts with explicit level indication: 0 = main target at bottom;
|
file |
diff |
annotate
|
| Thu, 22 Mar 2012 15:41:49 +0100 |
wenzelm |
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
|
file |
diff |
annotate
|
| Thu, 22 Mar 2012 10:49:31 +0100 |
wenzelm |
synchronize syntax uniformly for target stack and aux. context;
|
file |
diff |
annotate
|
| Thu, 22 Mar 2012 10:10:30 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 11:25:19 +0100 |
wenzelm |
clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2);
|
file |
diff |
annotate
|
| Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
| Wed, 14 Mar 2012 18:09:05 +0100 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Wed, 14 Mar 2012 15:23:50 +0100 |
wenzelm |
more indentation;
|
file |
diff |
annotate
|
| Wed, 14 Mar 2012 14:49:43 +0100 |
wenzelm |
eliminated obsolete sanitize_name;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 20:47:11 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 21:17:45 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 05 Nov 2011 15:00:49 +0100 |
wenzelm |
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
|
file |
diff |
annotate
|
| Sun, 30 Oct 2011 22:20:45 +0100 |
wenzelm |
removed obsolete argument (cf. aa35859c8741);
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 23:16:50 +0200 |
wenzelm |
refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 22:17:30 +0200 |
wenzelm |
uniform Local_Theory.declaration with explicit params;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 14:57:09 +0200 |
wenzelm |
simplified check/uncheck interfaces: result comparison is hardwired by default;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 13:52:23 +0200 |
wenzelm |
standardized aliases of operations on tsig;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 13:26:39 +0200 |
wenzelm |
pass plain Proof.context for pretty printing;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 12:04:21 +0200 |
wenzelm |
simplified Sorts.class_error: plain Proof.context;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 11:13:29 +0200 |
wenzelm |
simplified pretty printing context, which is only required for certain kernel operations;
|
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, 18 Dec 2010 18:43:13 +0100 |
ballarin |
Add mixins to sublocale command.
|
file |
diff |
annotate
|
| Sat, 20 Nov 2010 00:53:26 +0100 |
wenzelm |
renamed raw "explode" function to "raw_explode" 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
|
| Thu, 16 Sep 2010 15:37:12 +0200 |
wenzelm |
Isar "default" step needs to fail for solved problems, for clear distinction of '.' and '..' for example -- amending lapse introduced in 9de4d64eee3b (April 2004);
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 16:15:12 +0200 |
haftmann |
more precise name for activation of improveable syntax
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 21:41:24 +0200 |
wenzelm |
turned show_sorts/show_types into proper configuration options;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 19:47:40 +0200 |
wenzelm |
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
|
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
|
| Fri, 20 Aug 2010 08:52:01 +0200 |
haftmann |
tuned: less formal noise in Named_Target, more coherence in Class
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 13:53:42 +0200 |
haftmann |
Class.declare -> Class.const
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 20:25:44 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 17:59:32 +0200 |
haftmann |
tuned internal structure
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 17:19:27 +0200 |
haftmann |
remove reinit operation alltogether
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 16:02:03 +0200 |
haftmann |
more convenient split of class modules: class and class_declaration
|
file |
diff |
annotate
| base
|
| Wed, 11 Aug 2010 15:09:30 +0200 |
haftmann |
explicit accessed to structure Class_Target
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 18:22:14 +0200 |
wenzelm |
spelling;
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 14:45:38 +0200 |
haftmann |
renamed Theory_Target to the more appropriate Named_Target
|
file |
diff |
annotate
|
| Sat, 31 Jul 2010 21:14:20 +0200 |
ballarin |
Make registrations generic data.
|
file |
diff |
annotate
|
| Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Reapply mixin patch: base for performance improvements.
|
file |
diff |
annotate
|
| Fri, 14 May 2010 21:23:29 +0200 |
ballarin |
Revert mixin patch due to inacceptable performance drop.
|
file |
diff |
annotate
|
| Thu, 13 May 2010 13:29:43 +0200 |
ballarin |
Remove improper use of mixin in class package.
|
file |
diff |
annotate
|
| Sat, 08 May 2010 19:18:28 +0200 |
wenzelm |
tuned error message: regular Pretty.string_of instead of raw Pretty.output;
|
file |
diff |
annotate
|
| Sat, 08 May 2010 19:14:13 +0200 |
wenzelm |
unified/simplified Pretty.margin_default;
|
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
|
| Wed, 05 May 2010 08:57:23 +0200 |
haftmann |
tuned interpunctation, dropped dead comment
|
file |
diff |
annotate
|
| Tue, 04 May 2010 14:44:30 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 04 May 2010 08:55:43 +0200 |
haftmann |
locale predicates of classes carry a mandatory "class" prefix
|
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
|
| Wed, 28 Apr 2010 13:30:52 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 13:30:34 +0200 |
haftmann |
try to observe intended meaning of add_registration interface more closely
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 13:29:39 +0200 |
haftmann |
empty class specifcations observe default sort
|
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
|
| Tue, 09 Mar 2010 14:35:02 +0100 |
wenzelm |
added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
|
file |
diff |
annotate
|
| Fri, 12 Feb 2010 09:49:28 +0100 |
haftmann |
tuned comments
|
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
|
| Tue, 10 Nov 2009 16:04:57 +0100 |
wenzelm |
modernized structure Theory_Target;
|
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
|
| Sat, 17 Oct 2009 16:58:03 +0200 |
wenzelm |
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
|
file |
diff |
annotate
|
| Wed, 07 Oct 2009 12:06:04 +0200 |
haftmann |
do not use Locale.add_registration_eqs any longer
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 17:11:48 +0200 |
haftmann |
proper merge of interpretation equations
|
file |
diff |
annotate
|
| Sun, 27 Sep 2009 09:52:25 +0200 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| Sat, 25 Jul 2009 18:44:55 +0200 |
haftmann |
improved handling of parameter import; tuned
|
file |
diff |
annotate
|
| Mon, 20 Jul 2009 16:49:05 +0200 |
haftmann |
dropped add_registration interface in locale
|
file |
diff |
annotate
|
| Fri, 10 Jul 2009 07:59:28 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 20:36:38 +0200 |
wenzelm |
clarified Thm.of_class/of_sort/class_triv;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 19:58:52 +0200 |
wenzelm |
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2009 21:26:18 +0200 |
wenzelm |
renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Wed, 17 Jun 2009 17:42:36 +0200 |
haftmann |
skip_proof where appropriate
|
file |
diff |
annotate
|
| Mon, 15 Jun 2009 08:16:09 +0200 |
haftmann |
skip_proof not operative here
|
file |
diff |
annotate
|
| Sun, 14 Jun 2009 17:20:19 +0200 |
haftmann |
using skip_proof where appropriate
|
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 16:00:54 +0100 |
wenzelm |
simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
|
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
|
| Sat, 07 Mar 2009 22:16:50 +0100 |
wenzelm |
more uniform handling of binding in targets and derived elements;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 11:32:31 +0100 |
wenzelm |
Binding.str_of: removed verbose feature, include qualifier in output;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 14:07:43 +0100 |
wenzelm |
Thm.binding;
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 09:05:20 +0100 |
haftmann |
more robust failure in error situations
|
file |
diff |
annotate
|
| Tue, 03 Feb 2009 21:26:21 +0100 |
haftmann |
handling type classes without parameters
|
file |
diff |
annotate
|
| Sun, 01 Feb 2009 19:58:02 +0100 |
haftmann |
proper declared constants in class expressions
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:35:42 +0100 |
haftmann |
explicit check for exactly one type variable in class specification elements
|
file |
diff |
annotate
|
| Mon, 26 Jan 2009 22:14:19 +0100 |
haftmann |
fixed reading of class specs: declare class operations in context
|
file |
diff |
annotate
|
| Mon, 26 Jan 2009 08:23:55 +0100 |
haftmann |
correct proof of assm_intro rule
|
file |
diff |
annotate
|
| Fri, 23 Jan 2009 19:51:49 +0100 |
haftmann |
fixed fixme
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:40:23 +0100 |
haftmann |
no base sort in class import
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:02 +0100 |
haftmann |
improved and corrected reading of class specs -- still draft version
|
file |
diff |
annotate
|
| Mon, 19 Jan 2009 08:16:42 +0100 |
haftmann |
improved tackling of subclasses
|
file |
diff |
annotate
|
| Sun, 18 Jan 2009 10:11:12 +0100 |
haftmann |
improved calculation of morphisms and rules
|
file |
diff |
annotate
|
| Sat, 17 Jan 2009 08:29:54 +0100 |
haftmann |
code cleanup
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 14:58:11 +0100 |
haftmann |
migrated class package to new locale implementation
|
file |
diff |
annotate
|
| Sun, 11 Jan 2009 14:18:16 +0100 |
haftmann |
construct explicit class morphism
|
file |
diff |
annotate
|
| Wed, 07 Jan 2009 08:03:25 +0100 |
haftmann |
proper local_theory after Class.class
|
file |
diff |
annotate
|
| Mon, 05 Jan 2009 15:55:04 +0100 |
haftmann |
locale -> old_locale, new_locale -> locale
|
file |
diff |
annotate
|
| Mon, 05 Jan 2009 15:36:24 +0100 |
haftmann |
rearranged target theories
|
file |
diff |
annotate
|
| Fri, 02 Jan 2009 08:13:12 +0100 |
haftmann |
improved boostrap order: theory_target.ML before expression.ML
|
file |
diff |
annotate
|
| Wed, 17 Dec 2008 12:10:39 +0100 |
haftmann |
temporary adaption to new locale code
|
file |
diff |
annotate
|
| Tue, 09 Dec 2008 13:11:42 +0100 |
ballarin |
NewLocale.intro_locales_tac added to Class.default_intro_tac.
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 18:43:42 +0100 |
haftmann |
Name.name_of -> Binding.base_name
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Mon, 01 Dec 2008 19:41:16 +0100 |
haftmann |
new Binding module
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 14:55:25 +0100 |
haftmann |
using name bindings
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 17:00:27 +0100 |
haftmann |
explicit name morphism function for locale interpretation
|
file |
diff |
annotate
|
| Thu, 13 Nov 2008 14:19:10 +0100 |
haftmann |
proper name morphisms for locales
|
file |
diff |
annotate
|
| Thu, 06 Nov 2008 09:09:48 +0100 |
haftmann |
class morphism stemming from locale interpretation
|
file |
diff |
annotate
|