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 |
Tue, 19 Sep 2006 15:21:51 +0200 | haftmann | dropped error-prone code generation 2 for wfrec | file | diff | annotate |