Sat, 13 Mar 2010 19:35:53 +0100 |
wenzelm |
minor tuning and simplification;
|
file |
diff |
annotate
|
Sat, 13 Mar 2010 14:41:14 +0100 |
wenzelm |
Local_Defs.contract convenience;
|
file |
diff |
annotate
|
Thu, 11 Mar 2010 23:45:41 +0100 |
wenzelm |
more basic Local_Defs.export_cterm;
|
file |
diff |
annotate
|
Sun, 07 Mar 2010 11:57:16 +0100 |
wenzelm |
modernized structure Local_Defs;
|
file |
diff |
annotate
|
Thu, 18 Feb 2010 23:41:01 +0100 |
wenzelm |
removed unused Theory_Target.begin;
|
file |
diff |
annotate
|
Mon, 15 Feb 2010 14:04:06 +0100 |
haftmann |
apply global morphism for theory, instantiation and overloading target; n.b. target morphism and global morphism coincide for theory target
|
file |
diff |
annotate
|
Thu, 19 Nov 2009 14:44:22 +0100 |
wenzelm |
Local_Theory.define: eliminated slightly odd kind argument -- such low-level definitions should be hardly ever exposed to end-users anyway;
|
file |
diff |
annotate
|
Tue, 17 Nov 2009 14:50:55 +0100 |
wenzelm |
uniform new_group/reset_group;
|
file |
diff |
annotate
|
Sun, 15 Nov 2009 19:45:05 +0100 |
wenzelm |
eliminated obsolete thm position tags;
|
file |
diff |
annotate
|
Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
Fri, 13 Nov 2009 20:41:29 +0100 |
wenzelm |
eliminated slightly odd kind argument of LocalTheory.note(s);
|
file |
diff |
annotate
|
Tue, 10 Nov 2009 16:04:57 +0100 |
wenzelm |
modernized structure Theory_Target;
|
file |
diff |
annotate
|
Mon, 09 Nov 2009 20:47:39 +0100 |
wenzelm |
locale_const/target_notation: uniform use of Term.aconv_untyped;
|
file |
diff |
annotate
|
Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
Fri, 06 Nov 2009 10:26:13 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
Wed, 04 Nov 2009 22:54:42 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Mon, 02 Nov 2009 21:27:26 +0100 |
ballarin |
Relax on type agreement with original context when applying term syntax.
|
file |
diff |
annotate
|
Thu, 05 Nov 2009 22:06:46 +0100 |
wenzelm |
allow "pervasive" local theory declarations, which are applied the background theory;
|
file |
diff |
annotate
|
Wed, 28 Oct 2009 17:38:13 +0100 |
wenzelm |
misc tuning;
|
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
|
Sun, 25 Oct 2009 19:18:59 +0100 |
wenzelm |
maintain group via name space, not tags;
|
file |
diff |
annotate
|
Wed, 30 Sep 2009 22:24:57 +0200 |
wenzelm |
eliminated redundant parameters;
|
file |
diff |
annotate
|
Wed, 15 Jul 2009 23:11:57 +0200 |
wenzelm |
eliminated obsolete legacy_varify;
|
file |
diff |
annotate
|
Thu, 09 Jul 2009 22:48:12 +0200 |
wenzelm |
renamed structure TermSubst to Term_Subst;
|
file |
diff |
annotate
|
Mon, 29 Jun 2009 16:17:57 +0200 |
haftmann |
mutual instances
|
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
|
Fri, 13 Mar 2009 19:17:58 +0100 |
haftmann |
coherent binding policy with primitive target operations
|
file |
diff |
annotate
|
Thu, 12 Mar 2009 15:54:58 +0100 |
wenzelm |
Assumption.all_prems_of, Assumption.all_assms_of;
|
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
|
Wed, 11 Mar 2009 15:45:40 +0100 |
wenzelm |
more precise treatment of qualified bindings;
|
file |
diff |
annotate
|
Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
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
|
Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
Thu, 05 Mar 2009 10:54:03 +0100 |
wenzelm |
Binding.prefix_of;
|
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
|
Wed, 18 Feb 2009 19:18:33 +0100 |
haftmann |
fixed signature
|
file |
diff |
annotate
|
Mon, 02 Feb 2009 13:56:23 +0100 |
haftmann |
strict check for locale target
|
file |
diff |
annotate
|
Wed, 21 Jan 2009 16:47:03 +0100 |
haftmann |
wrecked old locale package and related modules
|
file |
diff |
annotate
|
Wed, 07 Jan 2009 22:31:37 +0100 |
haftmann |
tuned siganture of locale.ML
|
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
|
Tue, 30 Dec 2008 11:10:01 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Fri, 19 Dec 2008 16:39:23 +0100 |
ballarin |
All logics ported to new locales.
|
file |
diff |
annotate
|
Fri, 12 Dec 2008 17:00:42 +0100 |
ballarin |
Theory target distinguishes old and new locales.
|
file |
diff |
annotate
|
Thu, 11 Dec 2008 18:30:26 +0100 |
ballarin |
Conversion of HOL-Main and ZF to new locales.
|
file |
diff |
annotate
|
Sat, 13 Dec 2008 17:46:13 +0100 |
wenzelm |
removed Ids;
|
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 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
|
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
|
Wed, 19 Nov 2008 16:58:33 +0100 |
ballarin |
Enable switching to new locales during session.
|
file |
diff |
annotate
|
Tue, 18 Nov 2008 09:41:23 +0100 |
ballarin |
Code for switching to new locales.
|
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 08:50:11 +0100 |
haftmann |
re-educated guess
|
file |
diff |
annotate
|
Thu, 06 Nov 2008 09:09:51 +0100 |
haftmann |
cleaned
|
file |
diff |
annotate
|
Tue, 28 Oct 2008 17:53:46 +0100 |
ballarin |
Revoked workaround (incompatible with HOL/ex/LocaleTest2.thy).
|
file |
diff |
annotate
|
Mon, 27 Oct 2008 16:20:52 +0100 |
ballarin |
Hide path in constant name (workaround).
|
file |
diff |
annotate
|