| Wed, 31 Dec 2008 19:54:03 +0100 |
wenzelm |
qualified Term.rename_wrt_term;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Sat, 13 Dec 2008 13:24:45 +0100 |
berghofe |
Modified nominal_primrec to make it work with local theories, unified syntax
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 18:43:42 +0100 |
haftmann |
Name.name_of -> Binding.base_name
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Tue, 07 Oct 2008 16:07:50 +0200 |
haftmann |
arbitrary is undefined
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:45 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 08:15:40 +0200 |
haftmann |
PureThy: dropped note_thmss_qualified, dropped _i suffix
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 13:03:07 +0100 |
wenzelm |
eliminated quiete_mode ref (unused);
|
file |
diff |
annotate
|
| Thu, 06 Dec 2007 15:10:09 +0100 |
haftmann |
added new primrec package
|
file |
diff |
annotate
|
| Mon, 08 Oct 2007 18:13:05 +0200 |
wenzelm |
turned keywords invariant/freshness_context into reserved indentifiers;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2007 16:50:04 +0200 |
wenzelm |
simplified interfaces for outer syntax;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 17:06:14 +0200 |
wenzelm |
proper Sign operations instead of Theory aliases;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 13:28:37 +0200 |
wenzelm |
Syntax.parse/check/read;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2007 22:35:34 +0200 |
wenzelm |
replaced ProofContext.infer_types by general Syntax.check_terms;
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:34:38 +0200 |
berghofe |
Moved unify_consts to PrimrecPackage.
|
file |
diff |
annotate
|
| Tue, 19 Jun 2007 23:15:27 +0200 |
wenzelm |
balanced conjunctions;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 00:01:51 +0200 |
wenzelm |
Method.Basic: include position;
|
file |
diff |
annotate
|
| Fri, 18 May 2007 11:12:03 +0200 |
berghofe |
Fixed bug in subst causing primrec functions returning functions
|
file |
diff |
annotate
|
| Wed, 18 Apr 2007 21:30:14 +0200 |
wenzelm |
simplified ProofContext.infer_types(_pats);
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 23:25:50 +0200 |
wenzelm |
removed obsolete TypeInfer.logicT -- use dummyT;
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 14:31:49 +0200 |
wenzelm |
proper ProofContext.infer_types;
|
file |
diff |
annotate
|
| Sat, 10 Mar 2007 16:31:55 +0100 |
berghofe |
- Replaced fold by fold_rev to make sure that list of predicate
|
file |
diff |
annotate
|
| Fri, 16 Feb 2007 19:19:19 +0100 |
berghofe |
Replaced "raise RecError" by "primrec_err" in function
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:08:08 +0100 |
wenzelm |
moved parts of OuterParse to SpecParse;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2006 16:53:00 +0100 |
berghofe |
nominal_primrec now prints initial proof state.
|
file |
diff |
annotate
|
| Fri, 01 Dec 2006 16:08:45 +0100 |
nipkow |
Added missing "standard"
|
file |
diff |
annotate
|
| Mon, 27 Nov 2006 12:10:51 +0100 |
berghofe |
Implemented new "nominal_primrec" command for defining
|
file |
diff |
annotate
|