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