| Fri, 25 Feb 2011 17:11:05 +0100 |
krauss |
fixed manual (rule no longer exists)
|
changeset |
files
|
| Fri, 25 Feb 2011 16:59:48 +0100 |
krauss |
removed support for tail-recursion from function package (now implemented by partial_function)
|
changeset |
files
|
| Fri, 25 Feb 2011 16:57:44 +0100 |
krauss |
reactivate time measurement (partly reverting c27b0b37041a);
|
changeset |
files
|
| Fri, 25 Feb 2011 16:57:43 +0100 |
krauss |
generalize find_theorems filters to work on raw propositions, too
|
changeset |
files
|
| Fri, 25 Feb 2011 14:25:52 +0100 |
nipkow |
merged
|
changeset |
files
|
| Fri, 25 Feb 2011 14:25:41 +0100 |
nipkow |
added simp lemma nth_Cons_pos to List
|
changeset |
files
|
| Fri, 25 Feb 2011 12:16:18 +0100 |
noschinl |
Refactor find_theorems to provide a more general filter_facts method
|
changeset |
files
|
| Fri, 25 Feb 2011 08:46:52 +0100 |
krauss |
removed dead code/unused exports/speculative generality
|
changeset |
files
|
| Thu, 24 Feb 2011 21:54:28 +0100 |
krauss |
recdef -> fun(ction)
|
changeset |
files
|
| Thu, 24 Feb 2011 20:52:05 +0100 |
krauss |
removed unused lemma
|
changeset |
files
|
| Thu, 24 Feb 2011 17:54:36 +0100 |
krauss |
recdef -> fun(ction);
|
changeset |
files
|
| Thu, 24 Feb 2011 17:38:05 +0100 |
krauss |
eliminated clones of List.upto
|
changeset |
files
|