| Sun, 28 Oct 2012 02:22:39 +0000 |
Christian Urban |
added function store_termination_rule to the signature, as it is used in Nominal2
|
file |
diff |
annotate
|
| Sun, 21 Oct 2012 22:31:39 +0200 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
| Sun, 21 Oct 2012 22:12:22 +0200 |
wenzelm |
proper signatures;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 20:07:00 +0100 |
wenzelm |
prefer formally checked @{keyword} parser;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 22:44:31 +0100 |
wenzelm |
discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component);
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 15:54:37 +0100 |
wenzelm |
comments;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 23:41:16 +0200 |
wenzelm |
tuned Named_Thms: proper binding;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 17:15:52 +0200 |
wenzelm |
tuned signature -- refined terminology;
|
file |
diff |
annotate
|
| Sun, 21 Aug 2011 20:42:26 +0200 |
wenzelm |
tuned Parse.group: delayed failure message;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 13:54:39 +0100 |
wenzelm |
indentation;
|
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
|
| Sun, 12 Dec 2010 21:41:01 +0100 |
krauss |
tuned headers
|
file |
diff |
annotate
|
| Fri, 10 Sep 2010 14:37:57 +0200 |
krauss |
improved error message for common mistake (fun f where "g x = ...")
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 21:41:24 +0200 |
wenzelm |
turned show_sorts/show_types into proper configuration options;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 21:04:22 +0200 |
wenzelm |
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 17:01:12 +0200 |
wenzelm |
theory data merge: prefer left side uniformly;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Sun, 16 May 2010 00:02:11 +0200 |
wenzelm |
prefer structure Parse_Spec;
|
file |
diff |
annotate
|
| Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 11:52:04 +0200 |
krauss |
default termination prover as plain tactic
|
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
|
| Thu, 19 Nov 2009 10:33:20 +0100 |
krauss |
check if equations are present for all functions to avoid low-level exception later
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
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
|
| Sun, 01 Nov 2009 20:59:34 +0100 |
wenzelm |
adapted Item_Net;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 20:47:10 +0200 |
krauss |
configuration flag "partials"
|
file |
diff |
annotate
|