src/Pure/Thy/thy_parse.ML
Tue, 20 Oct 1998 16:26:47 +0200 wenzelm Syntax.max_pri;
Tue, 04 Aug 1998 18:23:57 +0200 wenzelm added 'locale' section;
Sat, 20 Jun 1998 20:18:22 +0200 wenzelm export mk_triple1/2;
Mon, 25 May 1998 21:27:22 +0200 wenzelm tuned local, global;
Wed, 20 May 1998 18:56:59 +0200 wenzelm tuned keywords;
Wed, 29 Apr 1998 11:26:59 +0200 wenzelm replaced thy_setup by 'setup' section;
Sat, 04 Apr 1998 11:41:24 +0200 wenzelm replaced thy_data by thy_setup;
Mon, 09 Mar 1998 16:14:46 +0100 wenzelm tuned;
Mon, 29 Dec 1997 14:29:34 +0100 wenzelm removed distinct_fst_string;
Thu, 04 Dec 1997 13:49:27 +0100 wenzelm moved global_names ref to Pure/ROOT.ML;
Mon, 03 Nov 1997 21:04:51 +0100 wenzelm added MLtext section;
Mon, 03 Nov 1997 17:55:55 +0100 wenzelm tuned: distinct_fst_string;
Mon, 03 Nov 1997 14:09:16 +0100 wenzelm export const_decls parser;
Fri, 31 Oct 1997 15:28:01 +0100 wenzelm dup sections: warning instead of error;
Thu, 30 Oct 1997 17:00:34 +0100 wenzelm added thy_data;
Tue, 28 Oct 1997 17:32:38 +0100 wenzelm PureThy.add_store_defs, PureThy.add_store_axioms;
Mon, 27 Oct 1997 15:43:53 +0100 wenzelm flipped global_names default;
Thu, 23 Oct 1997 12:44:46 +0200 wenzelm improved typ parser, exported;
Mon, 20 Oct 1997 17:08:18 +0200 wenzelm make SML/NJ happy;
Mon, 20 Oct 1997 10:38:16 +0200 wenzelm local section;
Fri, 17 Oct 1997 11:10:54 +0200 paulson Eta-expanded a function decl to make sml/nj happy
Thu, 16 Oct 1997 14:48:10 +0200 wenzelm removed begin;
Wed, 15 Oct 1997 15:14:56 +0200 wenzelm eliminated aliasing merge: now always extends;
Thu, 09 Oct 1997 14:53:31 +0200 wenzelm improved oracle: name;
Mon, 06 Oct 1997 20:00:31 +0200 wenzelm fixed 'begin';
Mon, 06 Oct 1997 19:39:40 +0200 wenzelm optional begin keyword;
Mon, 06 Oct 1997 18:29:11 +0200 wenzelm added 'path' section;
Wed, 01 Oct 1997 18:19:44 +0200 wenzelm fully qualified name: Theory.set_oracle;
Wed, 01 Oct 1997 17:40:09 +0200 wenzelm fully qualified names: Theory.add_XXX;
Fri, 18 Jul 1997 13:36:03 +0200 wenzelm renamed |-> <-| <-> to Parse/PrintRule;
Tue, 06 May 1997 12:55:07 +0200 wenzelm removed MLtrans, MLtext;
Fri, 28 Feb 1997 16:40:08 +0100 wenzelm added token_translation interface;
Fri, 13 Dec 1996 17:37:42 +0100 wenzelm added typed print translations;
Tue, 10 Dec 1996 12:50:35 +0100 wenzelm syntax section: added 'output' mode option;
Wed, 27 Nov 1996 16:40:23 +0100 wenzelm use_thy now automatically opens theory structures;
Tue, 26 Nov 1996 16:33:59 +0100 paulson Eta-expansion of a function definition, for value polymorphism
Mon, 18 Nov 1996 17:31:14 +0100 wenzelm mixfix: added syntax for Infirl/rName;
Thu, 11 Jul 1996 15:18:57 +0200 paulson Oracles can now be strings instead of identifiers
Tue, 18 Jun 1996 16:17:38 +0200 paulson Translation infixes <->, etc., no longer available at top-level
Tue, 30 Apr 1996 13:40:32 +0200 clasohm changed ident_no_colon so that it forbids postfix "=", too
Wed, 06 Mar 1996 14:11:41 +0100 clasohm added constdefs
Tue, 05 Mar 1996 15:52:59 +0100 paulson Addition of oracles
Fri, 16 Feb 1996 18:00:47 +0100 paulson Elimination of fully-functorial style.
Fri, 01 Dec 1995 13:54:27 +0100 clasohm added const_type to type_decl
Fri, 01 Dec 1995 12:22:07 +0100 clasohm simplified parser for constType
Wed, 29 Nov 1995 16:47:38 +0100 clasohm added type class to simple_type
Tue, 07 Nov 1995 12:57:20 +0100 clasohm types in consts section of .thy files can now be specified without quotes
Wed, 06 Sep 1995 15:27:11 +0200 clasohm removed list2 and enum2
Wed, 06 Sep 1995 15:11:19 +0200 clasohm added enum2 and list2
Mon, 21 Aug 1995 18:03:12 +0200 wenzelm minor fix to make less noise with SML/NJ;
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).
Fri, 27 Jan 1995 13:40:07 +0100 wenzelm binder: optional body pri now [bracketted];
Wed, 18 Jan 1995 11:36:04 +0100 clasohm added optional precedence for body of binder;
Fri, 09 Dec 1994 16:44:31 +0100 wenzelm minor internal changes;
Wed, 07 Dec 1994 12:34:47 +0100 clasohm moved first call of store_theory from thy_read.ML to created .thy.ML file
Mon, 14 Nov 1994 11:57:32 +0100 wenzelm exported 'cat';
Tue, 25 Oct 1994 13:16:49 +0100 wenzelm strip_quotes now exported;
Wed, 12 Oct 1994 16:30:19 +0100 wenzelm type_args, opt_witness now exported;
Wed, 07 Sep 1994 10:43:30 +0200 clasohm renamed temporary variable 'base' to 'thy' in mk_structure
Tue, 06 Sep 1994 14:44:10 +0200 clasohm renamed base_on into mk_base and moved it to the beginning of the generated
less more (0) -60 tip