| Thu, 15 Mar 2012 20:07:00 +0100 |
prefer formally checked @{keyword} parser;
|
file | diff | annotate |
| Tue, 08 Nov 2011 11:44:37 +0100 |
tuned;
|
file | diff | annotate |
| Fri, 28 Oct 2011 23:41:16 +0200 |
tuned Named_Thms: proper binding;
|
file | diff | annotate |
| Tue, 20 Sep 2011 01:32:04 +0200 |
match types when applying mono_thm -- previous export generalizes type variables;
|
file | diff | annotate |
| Tue, 31 May 2011 11:16:52 +0200 |
generate raw induction rule as instance of generic rule with careful treatment of currying
|
file | diff | annotate |
| Mon, 23 May 2011 21:34:37 +0200 |
also manage induction rule;
|
file | diff | annotate |
| Mon, 23 May 2011 10:58:21 +0200 |
separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform
|
file | diff | annotate |
| Wed, 27 Apr 2011 21:50:04 +0200 |
clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
|
file | diff | annotate |
| Mon, 18 Apr 2011 13:52:23 +0200 |
standardized aliases of operations on tsig;
|
file | diff | annotate |
| Sat, 16 Apr 2011 16:15:37 +0200 |
modernized structure Proof_Context;
|
file | diff | annotate |
| Thu, 24 Mar 2011 16:56:19 +0100 |
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
|
file | diff | annotate |
| Sat, 08 Jan 2011 17:14:48 +0100 |
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
|
file | diff | annotate |
| Mon, 13 Dec 2010 10:15:27 +0100 |
eliminated dest_all_all_ctx
|
file | diff | annotate |
| Tue, 26 Oct 2010 14:11:34 +0200 |
partial_function is a declaration command
|
file | diff | annotate |
| Tue, 26 Oct 2010 13:19:31 +0200 |
fixed confusion introduced in 008dc2d2c395
|
file | diff | annotate |
| Tue, 26 Oct 2010 12:19:02 +0200 |
added Spec_Rule declaration to partial_function
|
file | diff | annotate |
| Tue, 26 Oct 2010 12:19:01 +0200 |
declare recursive equation as ".simps", in accordance with other packages
|
file | diff | annotate |
| Sat, 23 Oct 2010 23:41:19 +0200 |
first version of partial_function package
|
file | diff | annotate |