src/HOL/Nominal/nominal_primrec.ML
Tue, 25 Sep 2007 13:28:37 +0200 wenzelm Syntax.parse/check/read;
Thu, 30 Aug 2007 22:35:34 +0200 wenzelm replaced ProofContext.infer_types by general Syntax.check_terms;
Wed, 11 Jul 2007 11:34:38 +0200 berghofe Moved unify_consts to PrimrecPackage.
Tue, 19 Jun 2007 23:15:27 +0200 wenzelm balanced conjunctions;
Wed, 13 Jun 2007 00:01:51 +0200 wenzelm Method.Basic: include position;
Fri, 18 May 2007 11:12:03 +0200 berghofe Fixed bug in subst causing primrec functions returning functions
Wed, 18 Apr 2007 21:30:14 +0200 wenzelm simplified ProofContext.infer_types(_pats);
Sun, 15 Apr 2007 23:25:50 +0200 wenzelm removed obsolete TypeInfer.logicT -- use dummyT;
Sun, 15 Apr 2007 14:31:49 +0200 wenzelm proper ProofContext.infer_types;
Sat, 10 Mar 2007 16:31:55 +0100 berghofe - Replaced fold by fold_rev to make sure that list of predicate
Fri, 16 Feb 2007 19:19:19 +0100 berghofe Replaced "raise RecError" by "primrec_err" in function
Fri, 19 Jan 2007 22:08:08 +0100 wenzelm moved parts of OuterParse to SpecParse;
Mon, 11 Dec 2006 16:53:00 +0100 berghofe nominal_primrec now prints initial proof state.
Fri, 01 Dec 2006 16:08:45 +0100 nipkow Added missing "standard"
Mon, 27 Nov 2006 12:10:51 +0100 berghofe Implemented new "nominal_primrec" command for defining
less more (0) tip