Sun, 29 Mar 2009 19:41:04 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sun, 29 Mar 2009 18:06:14 +0200 |
wenzelm |
simplified Element.activate(_i): singleton version;
|
file |
diff |
annotate
|
Sun, 29 Mar 2009 17:47:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sun, 29 Mar 2009 16:13:44 +0200 |
wenzelm |
unified binding prefix terminology;
|
file |
diff |
annotate
|
Sat, 28 Mar 2009 20:25:23 +0100 |
wenzelm |
simplified Locale.activate operations, using generic context;
|
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:49 +0100 |
wenzelm |
define_prefs: removed redundant Drule.gen_all, which is already part of the norm_hhf stage of Assumption.assume;
|
file |
diff |
annotate
|
Sat, 28 Mar 2009 16:00:54 +0100 |
wenzelm |
simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
|
file |
diff |
annotate
|
Thu, 26 Mar 2009 17:00:59 +0100 |
wenzelm |
register_locale: produce stamps at the spot where elements are registered;
|
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
|
Thu, 12 Mar 2009 13:18:42 +0100 |
wenzelm |
renamed sticky_prefix to mandatory_path;
|
file |
diff |
annotate
|
Thu, 12 Mar 2009 12:04:27 +0100 |
wenzelm |
replaced old-style add_path/no_base_names by sticky_prefix;
|
file |
diff |
annotate
|
Wed, 11 Mar 2009 15:38:25 +0100 |
wenzelm |
Thm.def_binding_optional;
|
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
|
Sat, 07 Mar 2009 11:32:31 +0100 |
wenzelm |
Binding.str_of: removed verbose feature, include qualifier in output;
|
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:12:52 +0100 |
wenzelm |
Binding.str_of;
|
file |
diff |
annotate
|
Sun, 01 Mar 2009 16:48:06 +0100 |
wenzelm |
discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
|
file |
diff |
annotate
|
Tue, 03 Feb 2009 21:26:21 +0100 |
haftmann |
handling type classes without parameters
|
file |
diff |
annotate
|
Sun, 01 Feb 2009 19:58:02 +0100 |
haftmann |
proper declared constants in class expressions
|
file |
diff |
annotate
|
Wed, 21 Jan 2009 22:26:49 +0100 |
wenzelm |
eliminated obsolete var morphism;
|
file |
diff |
annotate
|
Wed, 21 Jan 2009 16:47:03 +0100 |
haftmann |
refined witness algebra
|
file |
diff |
annotate
|
Mon, 19 Jan 2009 08:16:43 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
Sat, 17 Jan 2009 08:29:40 +0100 |
haftmann |
explicit equation morphism
|
file |
diff |
annotate
|
Fri, 16 Jan 2009 14:58:12 +0100 |
haftmann |
corrected preparation of instances: parameters are proper names, not raw terms
|
file |
diff |
annotate
|
Fri, 16 Jan 2009 08:04:38 +0100 |
haftmann |
added cert_read_declaration; more exports; tuned signature
|
file |
diff |
annotate
|
Thu, 15 Jan 2009 14:52:25 +0100 |
haftmann |
tuned interpretation code
|
file |
diff |
annotate
|
Sun, 11 Jan 2009 14:18:17 +0100 |
haftmann |
explicit bookkeeping of intro rules and axiom
|
file |
diff |
annotate
|