| Mon, 26 Oct 2009 23:27:16 +0100 |
krauss |
authentic constants; moved "acyclic" further down
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 23:26:57 +0100 |
krauss |
point-free characterization of well-foundedness
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 23:26:18 +0100 |
krauss |
replaced (outdated) comments by explicit statements
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:32:53 +0200 |
haftmann |
simplified proof
|
file |
diff |
annotate
|
| Mon, 31 Aug 2009 20:34:48 +0200 |
krauss |
moved lemma Wellfounded.in_inv_image to Relation.thy
|
file |
diff |
annotate
|
| Mon, 31 Aug 2009 20:34:44 +0200 |
krauss |
moved wfrec to Recdef.thy
|
file |
diff |
annotate
|
| Mon, 31 Aug 2009 20:32:00 +0200 |
krauss |
no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle
|
file |
diff |
annotate
|
| Tue, 28 Jul 2009 13:37:08 +0200 |
haftmann |
explicit is better than implicit
|
file |
diff |
annotate
|
| Tue, 28 Jul 2009 08:48:56 +0200 |
krauss |
moved obsolete same_fst to Recdef.thy
|
file |
diff |
annotate
|
| Mon, 27 Jul 2009 21:47:41 +0200 |
krauss |
"more standard" argument order of relation composition (op O)
|
file |
diff |
annotate
|
| Sat, 25 Jul 2009 18:44:55 +0200 |
haftmann |
explicit is better than implicit
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:09:30 +0200 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
|
| Sun, 26 Apr 2009 20:23:09 +0200 |
haftmann |
reverted slip in theory imports
|
file |
diff |
annotate
|
| Sun, 26 Apr 2009 08:34:53 +0200 |
haftmann |
adjusted to changes in power syntax
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 08:45:47 +0100 |
haftmann |
explicit code equations for some rarely used pred operations
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:40:23 +0100 |
haftmann |
changed import hierarchy
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:31 +0100 |
haftmann |
dropped ID
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 08:46:07 +0100 |
krauss |
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
|
file |
diff |
annotate
|
| Tue, 18 Nov 2008 21:17:14 +0100 |
krauss |
removed lemmas called lemma1 and lemma2
|
file |
diff |
annotate
|
| Wed, 12 Nov 2008 17:23:22 +0100 |
krauss |
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Tue, 07 Oct 2008 16:07:50 +0200 |
haftmann |
arbitrary is undefined
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 15:59:23 +0200 |
krauss |
wf_finite_psubset[simp], in_finite_psubset[simp]
|
file |
diff |
annotate
|
| Mon, 11 Aug 2008 14:49:53 +0200 |
haftmann |
moved class wellorder to theory Orderings
|
file |
diff |
annotate
|
| Fri, 23 May 2008 17:19:24 +0200 |
krauss |
rearranged subsections
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:56:52 +0200 |
berghofe |
- Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
|
file |
diff |
annotate
|
| Fri, 25 Apr 2008 15:30:33 +0200 |
krauss |
Merged theories about wellfoundedness into one: Wellfounded.thy
|
file |
diff |
annotate
|