| Fri, 07 Mar 2008 13:53:04 +0100 |
haftmann |
whitespace tuning
|
file |
diff |
annotate
|
| Thu, 28 Feb 2008 12:56:30 +0100 |
wenzelm |
wf_trancl: structured proof;
|
file |
diff |
annotate
|
| Thu, 21 Feb 2008 17:33:58 +0100 |
nipkow |
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
|
file |
diff |
annotate
|
| Fri, 15 Feb 2008 16:09:12 +0100 |
haftmann |
<= and < on nat no longer depend on wellfounded relations
|
file |
diff |
annotate
|
| Wed, 06 Feb 2008 16:06:40 +0100 |
krauss |
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
|
file |
diff |
annotate
|
| Tue, 13 Nov 2007 11:02:55 +0100 |
berghofe |
Removed some case_names and consumes attributes that are now no longer
|
file |
diff |
annotate
|
| Fri, 26 Oct 2007 21:22:18 +0200 |
haftmann |
dropped square syntax
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:11:39 +0200 |
berghofe |
Adapted to changes in infrastructure for converting between
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 18:33:31 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Fri, 01 Jun 2007 15:14:05 +0200 |
krauss |
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:50:17 +0200 |
haftmann |
changed code generator invocation syntax
|
file |
diff |
annotate
|
| Sat, 21 Apr 2007 19:32:32 +0200 |
huffman |
faster proof of wf_eq_minimal
|
file |
diff |
annotate
|
| Fri, 02 Mar 2007 15:43:21 +0100 |
haftmann |
now using "class"
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 17:29:41 +0100 |
berghofe |
- Adapted to new inductive definition package
|
file |
diff |
annotate
|