| Tue, 12 Apr 2016 14:38:57 +0200 |
wenzelm |
Type_Infer.object_logic controls improvement of type inference result;
|
file |
diff |
annotate
|
| Wed, 30 Mar 2016 23:34:00 +0200 |
wenzelm |
reconcile object-logic constraint vs. mixfix constraint;
|
file |
diff |
annotate
|
| Sun, 13 Dec 2015 21:56:15 +0100 |
wenzelm |
more general types Proof.method / context_tactic;
|
file |
diff |
annotate
|
| Fri, 04 Sep 2015 13:39:20 +0200 |
wenzelm |
trim context for persistent storage;
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 15:43:45 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 10:57:11 +0200 |
wenzelm |
avoid dynamic parsing of hardwired strings;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 23:01:46 +0100 |
wenzelm |
just one data slot per program unit;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 19:01:49 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 13:42:38 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 19:20:11 +0200 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| Fri, 09 May 2014 22:04:50 +0200 |
wenzelm |
more position markup to help locating the query context, e.g. from "Info" dockable;
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 18:19:57 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 21:32:41 +0100 |
blanchet |
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
|
file |
diff |
annotate
|
| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 22:10:17 +0200 |
krauss |
omit automatic Induct.cases_pred declaration, which breaks many existing proofs
|
file |
diff |
annotate
|
| Sun, 08 Sep 2013 23:26:08 +0200 |
krauss |
clarified
|
file |
diff |
annotate
|
| Sun, 08 Sep 2013 22:32:47 +0200 |
Manuel Eberl |
generate elim rules for elimination of function equalities;
|
file |
diff |
annotate
|
| Sun, 16 Jun 2013 22:56:44 +0200 |
krauss |
export dom predicate in the info record
|
file |
diff |
annotate
|
| Sun, 16 Jun 2013 01:39:00 +0200 |
krauss |
export cases rule in the info record
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Tue, 08 Jan 2013 16:01:07 +0100 |
wenzelm |
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
|
file |
diff |
annotate
|
| Sun, 21 Oct 2012 22:32:22 +0200 |
wenzelm |
recovered explicit error message, which was lost in b8570ea1ce25;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 12:18:21 +0200 |
wenzelm |
more precise indentation;
|
file |
diff |
annotate
|
| Mon, 23 Apr 2012 21:44:36 +0200 |
wenzelm |
more standard method setup;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 21:18:38 +0100 |
wenzelm |
added ML antiquotation @{attributes};
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 22:17:30 +0200 |
wenzelm |
uniform Local_Theory.declaration with explicit params;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 17:15:52 +0200 |
wenzelm |
tuned signature -- refined terminology;
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 16:30:38 +0200 |
wenzelm |
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 22:04:07 +0200 |
wenzelm |
less verbosity in batch mode -- spam reduction and notable performance improvement;
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 13:29:54 +0200 |
wenzelm |
slightly more uniform messages;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 15:39:55 +0200 |
wenzelm |
pervasive Output operations;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Fri, 25 Feb 2011 16:59:48 +0100 |
krauss |
removed support for tail-recursion from function package (now implemented by partial_function)
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 21:52:41 +0100 |
krauss |
function (default) is legacy feature
|
file |
diff |
annotate
|
| Mon, 27 Dec 2010 12:33:21 +0100 |
krauss |
function (tailrec) is a legacy feature
|
file |
diff |
annotate
|
| Sun, 12 Dec 2010 21:41:01 +0100 |
krauss |
tuned headers
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 23:45:20 +0200 |
krauss |
some cleanup in Function_Lib
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 09:54:07 +0200 |
krauss |
no longer declare .psimps rules as [simp].
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Thu, 27 May 2010 17:41:27 +0200 |
wenzelm |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 13:47:39 +0200 |
krauss |
return updated info record after termination proof
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 16:13:17 +0200 |
krauss |
return info record (relative to auxiliary context!)
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 10:31:15 +0200 |
krauss |
function: sane interface for programmatic use
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 09:48:22 +0200 |
krauss |
ML interface uses plain command names, following conventions from typedef
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 09:21:48 +0200 |
krauss |
function: better separate Isar integration from actual functionality
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 15:52:03 +0200 |
wenzelm |
modernized naming conventions of main Isar proof elements;
|
file |
diff |
annotate
|
| Fri, 12 Mar 2010 12:14:30 +0100 |
bulwahn |
refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 23:51:31 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 13:36:15 +0100 |
bulwahn |
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
|
file |
diff |
annotate
|
| Mon, 18 Jan 2010 10:34:27 +0100 |
krauss |
function package: declare Spec_Rules for simps from total functions, but not psimps or tail-rec equations
|
file |
diff |
annotate
|
| Sat, 02 Jan 2010 23:18:58 +0100 |
krauss |
new year's resolution: reindented code in function package
|
file |
diff |
annotate
|
| Sat, 02 Jan 2010 23:18:58 +0100 |
krauss |
provide simp and induct rules in Function.info
|
file |
diff |
annotate
|
| Sat, 02 Jan 2010 23:18:58 +0100 |
krauss |
more official data record Function.info
|
file |
diff |
annotate
|