| Sun, 29 Mar 2009 18:06:14 +0200 |
wenzelm |
simplified Element.activate(_i): singleton version;
|
file |
diff |
annotate
|
| Sun, 29 Mar 2009 17:47:50 +0200 |
wenzelm |
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
|
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
|
| 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
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
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:38:25 +0100 |
wenzelm |
Thm.def_binding_optional;
|
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 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:09 +0100 |
wenzelm |
Binding.str_of;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 14:07:43 +0100 |
wenzelm |
Thm.binding;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 22:26:48 +0100 |
wenzelm |
eliminated obsolete var morphism;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:03 +0100 |
haftmann |
refined witness algebra
|
file |
diff |
annotate
|
| Sat, 17 Jan 2009 08:29:40 +0100 |
haftmann |
explicit equation morphism
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 20:18:46 +0100 |
ballarin |
Transfer morphism with theory closure.
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 15:08:08 +0100 |
ballarin |
Finer-grained activation so that facts from earlier elements are available.
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 12:08:10 +0100 |
ballarin |
Use correct mode when parsing elements and conclusion.
|
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
|
| Tue, 25 Nov 2008 18:07:33 +0100 |
ballarin |
Use standard export function.
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 14:55:28 +0100 |
haftmann |
tuned name bindings
|
file |
diff |
annotate
|
| Wed, 19 Nov 2008 17:00:00 +0100 |
ballarin |
Basic types not qualified.
|
file |
diff |
annotate
|
| Tue, 18 Nov 2008 09:40:06 +0100 |
ballarin |
Activate elements moved to element.ML.
|
file |
diff |
annotate
|
| Thu, 13 Nov 2008 14:19:07 +0100 |
haftmann |
diagnostic output for name bindings
|
file |
diff |
annotate
|
| Mon, 10 Nov 2008 19:42:21 +0100 |
haftmann |
more verbose element printing
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 16:55:33 +0200 |
wenzelm |
type Attrib.binding abbreviates Name.binding without attributes;
|
file |
diff |
annotate
|