| Thu, 12 Mar 2009 13:18:42 +0100 |
wenzelm |
renamed sticky_prefix to mandatory_path;
|
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:44:12 +0100 |
wenzelm |
removed obsolete absolute_path -- use root_path with qualified binding;
|
file |
diff |
annotate
|
| Tue, 10 Mar 2009 21:20:01 +0100 |
wenzelm |
explicit root_path, parent_path;
|
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:12:07 +0100 |
wenzelm |
replace old bstring by binding for logical primitives: class, type, const etc.;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
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:09:08 +0100 |
wenzelm |
Binding.str_of;
|
file |
diff |
annotate
|
| Fri, 27 Feb 2009 16:38:52 +0100 |
wenzelm |
eliminated NJ's List.nth;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:32 +0100 |
haftmann |
binding is alias for Binding.T
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 18:43:42 +0100 |
haftmann |
Name.name_of -> Binding.base_name
|
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 19:06:02 +0100 |
haftmann |
dropped legacy naming code
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 14:55:25 +0100 |
haftmann |
using name bindings
|
file |
diff |
annotate
|
| Fri, 14 Nov 2008 08:50:10 +0100 |
haftmann |
namify and name_decl combinators
|
file |
diff |
annotate
|
| Wed, 03 Sep 2008 17:47:34 +0200 |
wenzelm |
declare_const: Name.binding, store/report position;
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 11:48:54 +0200 |
wenzelm |
type Properties.T;
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 21:00:26 +0200 |
haftmann |
type constructors now with markup
|
file |
diff |
annotate
|
| Thu, 19 Jun 2008 22:05:01 +0200 |
wenzelm |
moved get_sort to Isar/proof_context.ML;
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 18:55:05 +0200 |
wenzelm |
removed obsolete term reading operations (cf. old_goals.ML for legacy emulations);
|
file |
diff |
annotate
|
| Sat, 14 Jun 2008 17:26:14 +0200 |
wenzelm |
certify_term: reject qualified frees;
|
file |
diff |
annotate
|
| Fri, 13 Jun 2008 21:04:42 +0200 |
wenzelm |
map_const: soft version, no failure here;
|
file |
diff |
annotate
|
| Fri, 23 May 2008 21:20:26 +0200 |
wenzelm |
add constants: set Markup.theory_nameN in tags;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| Sat, 17 May 2008 14:27:01 +0200 |
wenzelm |
added pretty_global flag;
|
file |
diff |
annotate
|