| Tue, 31 Mar 2009 13:34:48 +0200 |
wenzelm |
tuned error message;
|
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 17:08:18 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 16:31:16 +0100 |
wenzelm |
replaced add_binds(_i) by bind_terms -- internal version only;
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 15:18:50 +0100 |
wenzelm |
pretty_thm_aux etc.: explicit show_status flag;
|
file |
diff |
annotate
|
| Sat, 21 Mar 2009 20:00:23 +0100 |
wenzelm |
removed obsolete pprint operations;
|
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
|
| Wed, 18 Mar 2009 21:55:38 +0100 |
wenzelm |
de-camelized Symbol_Pos;
|
file |
diff |
annotate
|
| Tue, 17 Mar 2009 16:55:21 +0100 |
wenzelm |
reverted abbreviations: improved performance via Item_Net.T;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 15:54:58 +0100 |
wenzelm |
Assumption.all_prems_of, Assumption.all_assms_of;
|
file |
diff |
annotate
|
| 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
|
| Tue, 10 Mar 2009 22:49:56 +0100 |
wenzelm |
Consts.eq_const is back again (cf. 907da436f8a9) -- required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;
|
file |
diff |
annotate
|
| Tue, 10 Mar 2009 21:19:22 +0100 |
wenzelm |
removed obsolete no_base_names;
|
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
|
| Thu, 05 Mar 2009 15:27:07 +0100 |
wenzelm |
eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 11:58:53 +0100 |
wenzelm |
eliminated obsolete ProofContext.full_bname;
|
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
|
| Tue, 03 Mar 2009 14:07:43 +0100 |
wenzelm |
Thm.binding;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 23:36:12 +0100 |
wenzelm |
use long names for old-style fold combinators;
|
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, 02 Jan 2009 19:38:13 +0100 |
wenzelm |
added numeral, which supercedes num, xnum, float;
|
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
|