| Mon, 20 Jan 2014 21:32:41 +0100 | blanchet | moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain | file | diff | annotate |
| Thu, 05 Dec 2013 09:20:32 +0100 | Andreas Lochbihler | restrict admissibility to non-empty chains to allow more syntax-directed proof rules | file | diff | annotate |
| Fri, 27 Sep 2013 12:26:23 +0200 | Andreas Lochbihler | generalise lemma | file | diff | annotate |
| Mon, 02 Sep 2013 16:28:11 +0200 | Andreas Lochbihler | move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems | file | diff | annotate |
| Wed, 24 Jul 2013 17:15:59 +0200 | krauss | derive specialized version of full fixpoint induction (with admissibility) | file | diff | annotate |
| Fri, 22 Mar 2013 00:39:16 +0100 | krauss | added rudimentary induction rule for partial_function (heap) | file | diff | annotate |
| Tue, 19 Mar 2013 13:19:21 +0100 | Andreas Lochbihler | add induction rule for partial_function (tailrec) | file | diff | annotate |