| 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
|
| Thu, 23 Oct 2008 15:28:01 +0200 |
wenzelm |
renamed Thm.get_axiom_i to Thm.axiom;
|
file |
diff |
annotate
|
| Wed, 22 Oct 2008 14:15:48 +0200 |
haftmann |
prove_instantiation_exit combinators
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 15:21:30 +0200 |
ballarin |
Public interface to interpretation morphism.
|
file |
diff |
annotate
|