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
|
Mon, 22 Sep 2008 08:00:28 +0200 |
haftmann |
temporary workaround for class constants
|
file |
diff |
annotate
|
Wed, 03 Sep 2008 17:47:40 +0200 |
wenzelm |
discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
|
file |
diff |
annotate
|
Tue, 02 Sep 2008 22:20:21 +0200 |
wenzelm |
tuned;
|
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
|
Tue, 29 Jul 2008 08:15:39 +0200 |
haftmann |
some steps towards explicit class target for canonical interpretation
|
file |
diff |
annotate
|
Sat, 21 Jun 2008 16:18:52 +0200 |
wenzelm |
import_export_proof: simplified thm definition -- PureThy.name_thm does the job;
|
file |
diff |
annotate
|
Sat, 12 Apr 2008 17:00:50 +0200 |
wenzelm |
removed unnecessary Goal.close_result;
|
file |
diff |
annotate
|
Mon, 25 Feb 2008 16:31:20 +0100 |
wenzelm |
implicit use of LocalTheory.group etc.;
|
file |
diff |
annotate
|
Sun, 10 Feb 2008 20:49:48 +0100 |
wenzelm |
tuned spaces;
|
file |
diff |
annotate
|
Sat, 09 Feb 2008 12:56:12 +0100 |
wenzelm |
overloading: reduced code redundancy, no xstrings here;
|
file |
diff |
annotate
|
Sat, 26 Jan 2008 17:08:43 +0100 |
wenzelm |
grouped versions of axioms/define/notes;
|
file |
diff |
annotate
|
Thu, 24 Jan 2008 23:51:20 +0100 |
wenzelm |
replaced ContextPosition by Position.thread_data;
|
file |
diff |
annotate
|
Tue, 08 Jan 2008 11:37:30 +0100 |
haftmann |
explicit type variables for instantiation
|
file |
diff |
annotate
|
Mon, 17 Dec 2007 22:40:14 +0100 |
haftmann |
note in target
|
file |
diff |
annotate
|
Tue, 11 Dec 2007 10:23:14 +0100 |
haftmann |
pretty for instantiation and overloading
|
file |
diff |
annotate
|
Mon, 10 Dec 2007 11:24:15 +0100 |
haftmann |
moved instance parameter management from class.ML to axclass.ML
|
file |
diff |
annotate
|
Wed, 05 Dec 2007 14:16:14 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
Mon, 03 Dec 2007 16:04:17 +0100 |
haftmann |
overloading target
|
file |
diff |
annotate
|
Fri, 30 Nov 2007 20:13:08 +0100 |
haftmann |
first working version of instance target
|
file |
diff |
annotate
|
Wed, 28 Nov 2007 09:01:42 +0100 |
haftmann |
tuned interfaces of class module
|
file |
diff |
annotate
|
Fri, 23 Nov 2007 21:09:35 +0100 |
haftmann |
rudimentary instantiation target
|
file |
diff |
annotate
|
Sun, 11 Nov 2007 14:17:15 +0100 |
wenzelm |
abbrev: back to PrintMode.internal, which works at least half-way;
|
file |
diff |
annotate
|
Sun, 11 Nov 2007 14:00:11 +0100 |
wenzelm |
abbrev: PrintMode.input instead of PrintMode.internal for global version!
|
file |
diff |
annotate
|
Sat, 10 Nov 2007 18:36:10 +0100 |
wenzelm |
removed LocalTheory.target_naming/name;
|
file |
diff |
annotate
|
Sat, 10 Nov 2007 14:31:22 +0100 |
wenzelm |
locale_const: suppress in class body as well (prevents qualified printing);
|
file |
diff |
annotate
|
Tue, 06 Nov 2007 22:50:38 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|