| Wed, 22 Jul 2009 11:23:09 +0200 |
wenzelm |
merged, resolving trivial conflict;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 16:14:51 +0200 |
haftmann |
dropped ancient flat_names option
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 01:03:18 +0200 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
| Fri, 10 Jul 2009 07:59:27 +0200 |
haftmann |
dropped find_index_eq
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 16:27:12 +0200 |
haftmann |
tuned interfaces of datatype module
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 15:32:34 +0200 |
haftmann |
add_datatypes does not yield particular rules any longer
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 14:50:34 +0200 |
haftmann |
add_datatype interface yields type names and less rules
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
| Tue, 16 Jun 2009 16:37:07 +0200 |
haftmann |
datatype packages: record datatype_config for configuration flags; less verbose signatures
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 16:11:04 +0200 |
haftmann |
avoid Library.foldl_map
|
file |
diff |
annotate
|
| Mon, 18 May 2009 09:48:06 +0200 |
haftmann |
introduced Thm.generatedK
|
file |
diff |
annotate
|
| Sat, 16 May 2009 20:17:59 +0200 |
bulwahn |
added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 14:14:02 +0100 |
wenzelm |
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2009 15:59:44 +0100 |
wenzelm |
simplified attribute setup;
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 15:42:19 +0100 |
wenzelm |
explicit Binding.qualified_name -- prevents implicitly qualified bstring;
|
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:17:25 +0100 |
wenzelm |
more uniform handling of binding in packages;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
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 16:47:04 +0100 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|
| Wed, 07 Jan 2009 23:53:08 +0100 |
wenzelm |
inductive: added fork_mono flag;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 20:31:36 +0100 |
wenzelm |
eliminated OldTerm.add_term_free_names;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 18:53:16 +0100 |
wenzelm |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Sun, 16 Nov 2008 20:03:42 +0100 |
wenzelm |
clarified Thm.proof_body_of vs. Thm.proof_of;
|
file |
diff |
annotate
|
| Sat, 15 Nov 2008 21:31:19 +0100 |
wenzelm |
name_of_thm: Proofterm.fold_proof_atoms;
|
file |
diff |
annotate
|
| Tue, 23 Sep 2008 15:48:50 +0200 |
wenzelm |
Thm.proof_of;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:45 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Sun, 24 Aug 2008 14:42:24 +0200 |
haftmann |
default replaces arbitrary
|
file |
diff |
annotate
|