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
|
Tue, 17 Nov 2009 14:51:57 +0100 |
wenzelm |
eliminated slightly odd name space grouping -- now managed by Isar toplevel;
|
file |
diff |
annotate
|
Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
Fri, 13 Nov 2009 20:41:29 +0100 |
wenzelm |
eliminated slightly odd kind argument of LocalTheory.note(s);
|
file |
diff |
annotate
|
Fri, 13 Nov 2009 17:25:09 +0100 |
wenzelm |
eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
|
file |
diff |
annotate
|
Tue, 10 Nov 2009 15:33:35 +0100 |
wenzelm |
removed unused Quickcheck_RecFun_Simps;
|
file |
diff |
annotate
|
Thu, 05 Nov 2009 22:08:47 +0100 |
wenzelm |
adapted LocalTheory.declaration;
|
file |
diff |
annotate
|
Mon, 02 Nov 2009 22:24:03 +0100 |
krauss |
conceal partial rules depending on config flag (i.e. when called via "fun")
|
file |
diff |
annotate
|
Mon, 02 Nov 2009 22:24:00 +0100 |
krauss |
conceal "termination" rule, used only by special tools
|
file |
diff |
annotate
|
Sun, 01 Nov 2009 15:44:26 +0100 |
wenzelm |
modernized structure Context_Rules;
|
file |
diff |
annotate
|
Sun, 01 Nov 2009 15:24:45 +0100 |
wenzelm |
modernized structure Rule_Cases;
|
file |
diff |
annotate
|
Sun, 25 Oct 2009 19:21:34 +0100 |
wenzelm |
name space groups are identified by serial, not serial_string;
|
file |
diff |
annotate
|
Sat, 24 Oct 2009 20:47:10 +0200 |
krauss |
configuration flag "partials"
|
file |
diff |
annotate
|