src/HOL/thy_syntax.ML
Wed, 10 Sep 1997 14:18:12 +0200 nipkow Added Larry's test for preventing a datatype shadowing a theory.
Wed, 06 Aug 1997 11:57:52 +0200 wenzelm use ThySyn.add_syntax;
Wed, 06 Aug 1997 01:18:31 +0200 berghofe Replaced "init_thy_reader" by "set_parser".
Mon, 23 Jun 1997 10:35:49 +0200 paulson New "congs" keyword for recdef theory section
Thu, 05 Jun 1997 13:22:25 +0200 paulson A slight simplification of optstring
Mon, 26 May 1997 12:42:38 +0200 paulson Now recdef checks the name of the function being defined.
Fri, 23 May 1997 09:17:26 +0200 nipkow Added overloaded function `size' for all datatypes.
Thu, 15 May 1997 12:53:12 +0200 paulson TFL theory section
Thu, 10 Apr 1997 12:20:55 +0200 nipkow Turned Addsimps into AddIffs for datatype laws.
Wed, 09 Apr 1997 12:32:04 +0200 paulson Using Blast_tac
Fri, 05 Jul 1996 14:22:59 +0200 berghofe Simplified syntax of primrec definitions.
Thu, 06 Jun 1996 13:13:18 +0200 paulson Quotes now optional around inductive set
Fri, 19 Apr 1996 11:33:24 +0200 clasohm added Konrad's code for the datatype package
Wed, 13 Mar 1996 11:55:25 +0100 clasohm modified primrec so it can be used in MiniML/Type.thy
Mon, 05 Feb 1996 21:27:16 +0100 clasohm expanded tabs; renamed subtype to typedef;
Tue, 30 Jan 1996 15:24:36 +0100 clasohm expanded tabs
Tue, 02 Jan 1996 10:46:50 +0100 paulson Improving space efficiency of inductive/datatype definitions.
Thu, 02 Nov 1995 12:45:58 +0100 clasohm extended complex_typ
Wed, 04 Oct 1995 13:10:03 +0100 clasohm added local simpsets; removed IOA from 'make test'
Fri, 08 Sep 1995 13:23:04 +0200 clasohm added nested types on right hand side of datatype definitions
Tue, 28 Mar 1995 12:25:20 +0200 clasohm changed syntax of datatype declarations (curried types for constructor
Fri, 03 Mar 1995 12:02:25 +0100 clasohm new version of HOL with curried function application
less more (0) tip