wenzelm [Tue, 03 Mar 2009 18:33:21 +0100] rev 30225
merged
nipkow [Tue, 03 Mar 2009 17:05:18 +0100] rev 30224
removed and renamed redundant lemmas
wenzelm [Tue, 03 Mar 2009 18:32:01 +0100] rev 30223
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;
minor tuning;
wenzelm [Tue, 03 Mar 2009 18:31:59 +0100] rev 30222
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
moved separator/is_qualified from binding.ML back to name_space.ML -- only name space introduces an explicit notation for qualified names;
type binding: maintain explicit qualifier, indepently of base name;
tuned signature of Binding: renamed name_pos to make, renamed base_name to name_of, renamed map_base to map_name, added mandatory flag to qualify, simplified map_prefix (formerly unused);
Binding.str_of: include markup with position properties;
misc tuning;
wenzelm [Tue, 03 Mar 2009 17:42:30 +0100] rev 30221
added markup for binding;
tuned;
wenzelm [Tue, 03 Mar 2009 15:12:52 +0100] rev 30220
Binding.str_of;
removed dead code;
tuned;
wenzelm [Tue, 03 Mar 2009 15:09:09 +0100] rev 30219
Binding.str_of;
pretty_name_atts: check Binding.is_empty, not result of Binding.str_of;