| 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
|
| 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
|