Fri, 18 Jul 1997 13:36:03 +0200 |
wenzelm |
renamed |-> <-| <-> to Parse/PrintRule;
|
file |
diff |
annotate
|
Tue, 06 May 1997 12:55:07 +0200 |
wenzelm |
removed MLtrans, MLtext;
|
file |
diff |
annotate
|
Fri, 28 Feb 1997 16:40:08 +0100 |
wenzelm |
added token_translation interface;
|
file |
diff |
annotate
|
Fri, 13 Dec 1996 17:37:42 +0100 |
wenzelm |
added typed print translations;
|
file |
diff |
annotate
|
Tue, 10 Dec 1996 12:50:35 +0100 |
wenzelm |
syntax section: added 'output' mode option;
|
file |
diff |
annotate
|
Wed, 27 Nov 1996 16:40:23 +0100 |
wenzelm |
use_thy now automatically opens theory structures;
|
file |
diff |
annotate
|
Tue, 26 Nov 1996 16:33:59 +0100 |
paulson |
Eta-expansion of a function definition, for value polymorphism
|
file |
diff |
annotate
|
Mon, 18 Nov 1996 17:31:14 +0100 |
wenzelm |
mixfix: added syntax for Infirl/rName;
|
file |
diff |
annotate
|
Thu, 11 Jul 1996 15:18:57 +0200 |
paulson |
Oracles can now be strings instead of identifiers
|
file |
diff |
annotate
|
Tue, 18 Jun 1996 16:17:38 +0200 |
paulson |
Translation infixes <->, etc., no longer available at top-level
|
file |
diff |
annotate
|
Tue, 30 Apr 1996 13:40:32 +0200 |
clasohm |
changed ident_no_colon so that it forbids postfix "=", too
|
file |
diff |
annotate
|
Wed, 06 Mar 1996 14:11:41 +0100 |
clasohm |
added constdefs
|
file |
diff |
annotate
|
Tue, 05 Mar 1996 15:52:59 +0100 |
paulson |
Addition of oracles
|
file |
diff |
annotate
|
Fri, 16 Feb 1996 18:00:47 +0100 |
paulson |
Elimination of fully-functorial style.
|
file |
diff |
annotate
|
Fri, 01 Dec 1995 13:54:27 +0100 |
clasohm |
added const_type to type_decl
|
file |
diff |
annotate
|
Fri, 01 Dec 1995 12:22:07 +0100 |
clasohm |
simplified parser for constType
|
file |
diff |
annotate
|
Wed, 29 Nov 1995 16:47:38 +0100 |
clasohm |
added type class to simple_type
|
file |
diff |
annotate
|
Tue, 07 Nov 1995 12:57:20 +0100 |
clasohm |
types in consts section of .thy files can now be specified without quotes
|
file |
diff |
annotate
|
Wed, 06 Sep 1995 15:27:11 +0200 |
clasohm |
removed list2 and enum2
|
file |
diff |
annotate
|
Wed, 06 Sep 1995 15:11:19 +0200 |
clasohm |
added enum2 and list2
|
file |
diff |
annotate
|
Mon, 21 Aug 1995 18:03:12 +0200 |
wenzelm |
minor fix to make less noise with SML/NJ;
|
file |
diff |
annotate
|
Tue, 11 Apr 1995 11:20:43 +0200 |
nipkow |
(binder "Q" p) generates Binder("Q",p,p); it used to be Binder("Q",0,p).
|
file |
diff |
annotate
|
Fri, 27 Jan 1995 13:40:07 +0100 |
wenzelm |
binder: optional body pri now [bracketted];
|
file |
diff |
annotate
|
Wed, 18 Jan 1995 11:36:04 +0100 |
clasohm |
added optional precedence for body of binder;
|
file |
diff |
annotate
|
Fri, 09 Dec 1994 16:44:31 +0100 |
wenzelm |
minor internal changes;
|
file |
diff |
annotate
|
Wed, 07 Dec 1994 12:34:47 +0100 |
clasohm |
moved first call of store_theory from thy_read.ML to created .thy.ML file
|
file |
diff |
annotate
|
Mon, 14 Nov 1994 11:57:32 +0100 |
wenzelm |
exported 'cat';
|
file |
diff |
annotate
|
Tue, 25 Oct 1994 13:16:49 +0100 |
wenzelm |
strip_quotes now exported;
|
file |
diff |
annotate
|
Wed, 12 Oct 1994 16:30:19 +0100 |
wenzelm |
type_args, opt_witness now exported;
|
file |
diff |
annotate
|
Wed, 07 Sep 1994 10:43:30 +0200 |
clasohm |
renamed temporary variable 'base' to 'thy' in mk_structure
|
file |
diff |
annotate
|