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
|
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
|