Thu, 12 Mar 2009 13:18:42 +0100 |
wenzelm |
renamed sticky_prefix to mandatory_path;
|
file |
diff |
annotate
|
Thu, 12 Mar 2009 12:04:27 +0100 |
wenzelm |
replaced old-style add_path/no_base_names by sticky_prefix;
|
file |
diff |
annotate
|
Wed, 11 Mar 2009 15:38:25 +0100 |
wenzelm |
Thm.def_binding_optional;
|
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 15:12:52 +0100 |
wenzelm |
Binding.str_of;
|
file |
diff |
annotate
|
Sun, 01 Mar 2009 16:48:06 +0100 |
wenzelm |
discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
|
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, 21 Jan 2009 22:26:49 +0100 |
wenzelm |
eliminated obsolete var morphism;
|
file |
diff |
annotate
|
Wed, 21 Jan 2009 16:47:03 +0100 |
haftmann |
refined witness algebra
|
file |
diff |
annotate
|
Mon, 19 Jan 2009 08:16:43 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
Sat, 17 Jan 2009 08:29:40 +0100 |
haftmann |
explicit equation morphism
|
file |
diff |
annotate
|
Fri, 16 Jan 2009 14:58:12 +0100 |
haftmann |
corrected preparation of instances: parameters are proper names, not raw terms
|
file |
diff |
annotate
|
Fri, 16 Jan 2009 08:04:38 +0100 |
haftmann |
added cert_read_declaration; more exports; tuned signature
|
file |
diff |
annotate
|
Thu, 15 Jan 2009 14:52:25 +0100 |
haftmann |
tuned interpretation code
|
file |
diff |
annotate
|
Sun, 11 Jan 2009 14:18:17 +0100 |
haftmann |
explicit bookkeeping of intro rules and axiom
|
file |
diff |
annotate
|
Wed, 07 Jan 2009 22:33:04 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
Wed, 07 Jan 2009 22:31:36 +0100 |
haftmann |
tuned signature; changed locale predicate name convention
|
file |
diff |
annotate
|
Wed, 07 Jan 2009 16:22:10 +0100 |
wenzelm |
qed/after_qed: singleton result;
|
file |
diff |
annotate
|
Tue, 06 Jan 2009 08:50:02 +0100 |
haftmann |
locale -> old_locale, new_locale -> locale
|
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
|
Thu, 01 Jan 2009 14:23:39 +0100 |
wenzelm |
avoid polymorphic equality;
|
file |
diff |
annotate
|
Wed, 31 Dec 2008 18:53:17 +0100 |
wenzelm |
use regular Term.add_XXX etc.;
|
file |
diff |
annotate
|
Tue, 30 Dec 2008 19:07:42 +0100 |
wenzelm |
prep_result: Thm.close_derivation of witness theorem avoids performance issues with proof terms;
|
file |
diff |
annotate
|
Tue, 23 Dec 2008 14:29:27 +0100 |
ballarin |
More liberal consistency check for defines elements.
|
file |
diff |
annotate
|
Fri, 19 Dec 2008 15:05:37 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Thu, 18 Dec 2008 11:16:48 +0100 |
Norbert Schirmer |
adapted statespace module to new locales;
|
file |
diff |
annotate
|
Fri, 19 Dec 2008 14:31:07 +0100 |
ballarin |
Intro_locales_tac knows about defines elements; more robust export morphism.
|
file |
diff |
annotate
|
Thu, 18 Dec 2008 20:19:49 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Wed, 17 Dec 2008 17:53:41 +0100 |
ballarin |
Prevent defines from being checked in interpretation.
|
file |
diff |
annotate
|
Thu, 18 Dec 2008 19:52:11 +0100 |
ballarin |
Refactored: evaluate specification text only in locale declarations.
|
file |
diff |
annotate
|
Tue, 16 Dec 2008 15:08:08 +0100 |
ballarin |
Finer-grained activation so that facts from earlier elements are available.
|
file |
diff |
annotate
|
Tue, 16 Dec 2008 12:08:10 +0100 |
ballarin |
Use correct mode when parsing elements and conclusion.
|
file |
diff |
annotate
|
Sun, 14 Dec 2008 15:43:04 +0100 |
ballarin |
Strict prefixes in locales expressions.
|
file |
diff |
annotate
|
Fri, 12 Dec 2008 12:31:00 +0100 |
ballarin |
Equations in interpretation as goals.
|
file |
diff |
annotate
|
Thu, 11 Dec 2008 17:56:34 +0100 |
ballarin |
Interpretation in theories: first version with equations.
|
file |
diff |
annotate
|
Wed, 10 Dec 2008 17:19:25 +0100 |
ballarin |
Use prefix component of bindings for locale prefixes.
|
file |
diff |
annotate
|
Wed, 10 Dec 2008 16:30:33 +0100 |
ballarin |
Preserve idents (expression in sublocale).
|
file |
diff |
annotate
|
Wed, 10 Dec 2008 14:21:42 +0100 |
ballarin |
Satisfy a_axioms.
|
file |
diff |
annotate
|
Wed, 10 Dec 2008 10:12:44 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Wed, 10 Dec 2008 10:11:18 +0100 |
ballarin |
Enable keyword 'structure' in for clause of locale expression.
|
file |
diff |
annotate
|
Tue, 09 Dec 2008 22:00:39 +0100 |
ballarin |
Correct order of defines in specification.
|
file |
diff |
annotate
|
Tue, 09 Dec 2008 21:27:00 +0100 |
ballarin |
Pass on defines in inheritance; reject illicit defines created by instantiation.
|
file |
diff |
annotate
|
Tue, 09 Dec 2008 15:34:49 +0100 |
ballarin |
Order of implicit parameters in locale expression.
|
file |
diff |
annotate
|
Tue, 09 Dec 2008 11:30:24 +0100 |
ballarin |
When adding locales, delay notes until local theory is built.
|
file |
diff |
annotate
|
Mon, 08 Dec 2008 21:33:50 +0100 |
ballarin |
Default names for definitions.
|
file |
diff |
annotate
|
Mon, 08 Dec 2008 18:44:24 +0100 |
ballarin |
Proper shape of assumptions generated from Defines elements.
|
file |
diff |
annotate
|
Mon, 08 Dec 2008 14:22:42 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Mon, 08 Dec 2008 14:18:29 +0100 |
ballarin |
Explicitly close up defines.
|
file |
diff |
annotate
|
Fri, 05 Dec 2008 16:41:36 +0100 |
ballarin |
Interpretation in proof contexts.
|
file |
diff |
annotate
|
Fri, 05 Dec 2008 18:43:42 +0100 |
haftmann |
Name.name_of -> Binding.base_name
|
file |
diff |
annotate
|
Fri, 05 Dec 2008 11:42:27 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Fri, 05 Dec 2008 11:26:07 +0100 |
ballarin |
Interpretation in theories including interaction with subclass relation.
|
file |
diff |
annotate
|
Fri, 05 Dec 2008 08:04:53 +0100 |
haftmann |
dropped NameSpace.declare_base
|
file |
diff |
annotate
|
Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|