| Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Avoid recomputation of registration instance for lookup.
|
file |
diff |
annotate
|
| Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Consistently use equality for registration lookup.
|
file |
diff |
annotate
|
| Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Cleaner implementation of sublocale command.
|
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:30:16 +0200 |
ballarin |
Add mixin to base morphism, required by class package; cf ab324ffd6f3d.
|
file |
diff |
annotate
|
| Tue, 04 May 2010 20:30:22 +0200 |
ballarin |
Merged.
|
file |
diff |
annotate
|
| Tue, 04 May 2010 19:57:55 +0200 |
ballarin |
Provide internal function for printing a single interpretation.
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 22:27:22 +0200 |
ballarin |
Explicitly manage export in dependencies.
|
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
|
| Tue, 20 Apr 2010 22:34:17 +0200 |
ballarin |
Remove garbage.
|
file |
diff |
annotate
|
| Tue, 20 Apr 2010 22:31:08 +0200 |
ballarin |
Remove garbage.
|
file |
diff |
annotate
|
| Wed, 07 Apr 2010 19:17:10 +0200 |
ballarin |
Merged resolving conflicts NEWS and locale.ML.
|
file |
diff |
annotate
|
| Fri, 02 Apr 2010 13:33:48 +0200 |
ballarin |
Proper inheritance of mixins for activated facts and locale dependencies.
|
file |
diff |
annotate
|
| Mon, 15 Feb 2010 19:54:54 +0100 |
ballarin |
Removed obsolete function.
|
file |
diff |
annotate
|
| Mon, 15 Feb 2010 01:34:08 +0100 |
ballarin |
Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 21:00:36 +0100 |
ballarin |
A rough implementation of full mixin inheritance; additional unit tests.
|
file |
diff |
annotate
|
| Tue, 02 Feb 2010 21:23:20 +0100 |
ballarin |
Clarified invariant; tuned.
|
file |
diff |
annotate
|
| Mon, 01 Feb 2010 21:55:00 +0100 |
ballarin |
Use serial to be more debug friendly.
|
file |
diff |
annotate
|
| Mon, 15 Mar 2010 18:59:16 +0100 |
wenzelm |
replaced type_syntax/term_syntax by uniform syntax_declaration;
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 22:02:11 +0100 |
wenzelm |
eliminated obsolete "internal" kind -- collapsed to unspecific "";
|
file |
diff |
annotate
|
| Mon, 09 Nov 2009 21:33:22 +0100 |
ballarin |
Removed obsolete code.
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 16:25:27 +0100 |
wenzelm |
conceal internal bindings;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 13:04:06 +0100 |
wenzelm |
make SML/NJ happy;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 20:54:08 +0200 |
wenzelm |
maintain explicit name space kind;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 19:47:37 +0200 |
wenzelm |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 19:20:03 +0200 |
wenzelm |
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 22:06:43 +0200 |
ballarin |
Observe order of declaration when printing registrations.
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 20:37:33 +0200 |
ballarin |
Avoid administrative overhead for identity mixins.
|
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
|
| Sun, 27 Sep 2009 11:50:27 +0200 |
ballarin |
Archive registrations by external view.
|
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
|
| Mon, 20 Jul 2009 16:49:05 +0200 |
haftmann |
dropped add_registration interface in locale
|
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:29 +0200 |
haftmann |
tuned locale interface
|
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:50 +0200 |
wenzelm |
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
|
file |
diff |
annotate
|
| Sun, 29 Mar 2009 16:13:24 +0200 |
wenzelm |
simplified roundup activation interface;
|
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:11 +0100 |
wenzelm |
renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
|
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
|
| Sat, 28 Mar 2009 12:48:31 +0100 |
wenzelm |
minor tuning;
|
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
|
| Fri, 13 Mar 2009 23:50:05 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 11:10:02 +0100 |
wenzelm |
renamed NameSpace.bind to NameSpace.define;
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 16:36:27 +0100 |
wenzelm |
eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
|
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
|
| 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
|
| Wed, 21 Jan 2009 16:47:03 +0100 |
haftmann |
wrecked old locale package and related modules
|
file |
diff |
annotate
|
| Sat, 17 Jan 2009 22:07:15 +0100 |
haftmann |
exported depedencies; tuned signature
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 08:04:39 +0100 |
haftmann |
tuned
|
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:31:36 +0100 |
haftmann |
tuned signature; internal code reorganisation
|
file |
diff |
annotate
|
| Tue, 06 Jan 2009 08:50:12 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 05 Jan 2009 15:55:51 +0100 |
haftmann |
locale -> old_locale, new_locale -> locale
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 18:53:19 +0100 |
wenzelm |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 15:30:10 +0100 |
wenzelm |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 18:42:37 +0100 |
haftmann |
removed Table.extend, NameSpace.extend_table
|
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
|
| Wed, 03 Dec 2008 15:26:46 +0100 |
ballarin |
Made global_note_qualified public.
|
file |
diff |
annotate
|
| Mon, 01 Dec 2008 19:41:16 +0100 |
haftmann |
new Binding module
|
file |
diff |
annotate
|
| Mon, 01 Dec 2008 16:02:57 +0100 |
haftmann |
Locale.*note* with conventional argument type
|
file |
diff |
annotate
|
| Mon, 01 Dec 2008 13:43:32 +0100 |
ballarin |
Methods intro_locales and unfold_locales apply to both old and new locales.
|
file |
diff |
annotate
|
| Thu, 27 Nov 2008 10:26:00 +0100 |
ballarin |
Fixed strange indentation.
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 19:06:05 +0100 |
haftmann |
Locale.local_note_qualified
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 14:55:28 +0100 |
haftmann |
tuned name bindings
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 17:00:27 +0100 |
haftmann |
explicit name morphism function for locale interpretation
|
file |
diff |
annotate
|
| Fri, 14 Nov 2008 14:00:52 +0100 |
ballarin |
Made local_note_prefix public.
|
file |
diff |
annotate
|
| Fri, 14 Nov 2008 08:50:10 +0100 |
haftmann |
namify and name_decl combinators
|
file |
diff |
annotate
|
| Thu, 13 Nov 2008 14:19:10 +0100 |
haftmann |
proper name morphisms for locales
|
file |
diff |
annotate
|
| Mon, 10 Nov 2008 19:42:22 +0100 |
haftmann |
restruced naming code in anticipation of introduction of name morphisms
|
file |
diff |
annotate
|
| Mon, 10 Nov 2008 08:18:58 +0100 |
haftmann |
using explicit interpretaton prefix in Name.binding (still on the surface)
|
file |
diff |
annotate
|
| Thu, 30 Oct 2008 10:57:45 +0100 |
ballarin |
Dropped context element 'includes'.
|
file |
diff |
annotate
|
| Mon, 27 Oct 2008 16:14:51 +0100 |
ballarin |
Extension of interface: declarations_of.
|
file |
diff |
annotate
|
| Fri, 26 Sep 2008 19:07:56 +0200 |
wenzelm |
eliminated polymorphic equality;
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 15:21:30 +0200 |
ballarin |
Public interface to interpretation morphism.
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 12:27:05 +0200 |
ballarin |
Clearer separation of interpretation frontend and backend.
|
file |
diff |
annotate
|
| Wed, 03 Sep 2008 17:47:30 +0200 |
wenzelm |
Sign.declare_const: Name.binding;
|
file |
diff |
annotate
|
| Wed, 03 Sep 2008 11:44:48 +0200 |
wenzelm |
Name.qualified;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 17:31:20 +0200 |
ballarin |
Interpretation commands no longer accept interpretation attributes.
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 16:55:33 +0200 |
wenzelm |
type Attrib.binding abbreviates Name.binding without attributes;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:45 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Thu, 28 Aug 2008 22:08:11 +0200 |
haftmann |
no parameter prefix for class interpretation
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 17:54:31 +0200 |
ballarin |
Consistent naming of theorems in interpretation.
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 12:00:28 +0200 |
wenzelm |
get rid of tabs;
|
file |
diff |
annotate
|
| Tue, 26 Aug 2008 16:04:22 +0200 |
ballarin |
Reorganisation of registration code.
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 16:52:46 +0200 |
wenzelm |
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
|
file |
diff |
annotate
|
| Wed, 06 Aug 2008 16:41:40 +0200 |
ballarin |
Interpretation command (theory/proof context) no longer simplifies goal.
|
file |
diff |
annotate
|
| Fri, 01 Aug 2008 17:41:37 +0200 |
ballarin |
Removed import and lparams from locale record.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2008 07:33:59 +0200 |
haftmann |
facts_of
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 08:15:44 +0200 |
haftmann |
tuned; explicit export of element accessors
|
file |
diff |
annotate
|
| Sat, 26 Jul 2008 09:00:26 +0200 |
haftmann |
tuned function name
|
file |
diff |
annotate
|
| Fri, 25 Jul 2008 12:03:32 +0200 |
haftmann |
dropped locale (open)
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:41 +0200 |
wenzelm |
Syntax.string_of_typ: proper context;
|
file |
diff |
annotate
|
| Mon, 14 Apr 2008 17:54:56 +0200 |
ballarin |
Changed naming scheme for theorems generated by interpretations.
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:48 +0200 |
wenzelm |
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 20:02:04 +0100 |
wenzelm |
Context.>> : operate on Context.generic;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 15:32:15 +0100 |
wenzelm |
eliminated delayed theory setup
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 00:20:49 +0100 |
wenzelm |
renamed former get_thms(_silent) to get_fact(_silent);
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 18:36:04 +0100 |
wenzelm |
closeup: recover original order of free variables!
|
file |
diff |
annotate
|
| Wed, 05 Mar 2008 22:58:11 +0100 |
wenzelm |
closeup: minor tuning of term traversal;
|
file |
diff |
annotate
|
| Mon, 17 Dec 2007 17:57:52 +0100 |
haftmann |
explicit closing of derived witnesses
|
file |
diff |
annotate
|
| Thu, 13 Dec 2007 07:09:07 +0100 |
haftmann |
memorizing and exporting destruction rules
|
file |
diff |
annotate
|
| Thu, 08 Nov 2007 22:19:43 +0100 |
wenzelm |
avoid "import" as identifier, which is a keyword in Alice;
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 17:48:51 +0100 |
ballarin |
Use of export rather than standard in interpretation.
|
file |
diff |
annotate
|
| Fri, 02 Nov 2007 18:53:01 +0100 |
haftmann |
generic tactic Method.intros_tac
|
file |
diff |
annotate
|
| Fri, 19 Oct 2007 12:22:12 +0200 |
ballarin |
Interpretation equations may have name and/or attribute;
|
file |
diff |
annotate
|
| Wed, 17 Oct 2007 23:16:34 +0200 |
wenzelm |
locale pred: authentic syntax, tuned aprop_tr' accordingly;
|
file |
diff |
annotate
|
| Wed, 17 Oct 2007 13:55:37 +0200 |
wenzelm |
clarified naming conventions of 'parse' and 'check' (as opposed to former 'cert');
|
file |
diff |
annotate
|
| Mon, 15 Oct 2007 15:29:43 +0200 |
haftmann |
canonical interpretation interface
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 14:42:30 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 10 Oct 2007 17:32:00 +0200 |
wenzelm |
removed redundant strip_vars/abs_eqn, use improved Drule.abs_def instead;
|
file |
diff |
annotate
|
| Wed, 10 Oct 2007 10:55:37 +0200 |
ballarin |
Prepare proper interface of interpretation_i, interpret_i.
|
file |
diff |
annotate
|