| Tue, 31 May 2011 11:16:52 +0200 |
krauss |
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 |
krauss |
also manage induction rule;
|
file |
diff |
annotate
|
| Mon, 23 May 2011 10:58:21 +0200 |
krauss |
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 |
wenzelm |
clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 13:52:23 +0200 |
wenzelm |
standardized aliases of operations on tsig;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 16:56:19 +0100 |
wenzelm |
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 |
wenzelm |
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 |
krauss |
eliminated dest_all_all_ctx
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 14:11:34 +0200 |
haftmann |
partial_function is a declaration command
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 13:19:31 +0200 |
krauss |
fixed confusion introduced in 008dc2d2c395
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 12:19:02 +0200 |
krauss |
added Spec_Rule declaration to partial_function
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 12:19:01 +0200 |
krauss |
declare recursive equation as ".simps", in accordance with other packages
|
file |
diff |
annotate
|
| Sat, 23 Oct 2010 23:41:19 +0200 |
krauss |
first version of partial_function package
|
file |
diff |
annotate
|