| 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 |
| Wed, 22 Aug 2012 22:55:41 +0200 | wenzelm | prefer ML_file over old uses; | file | diff | annotate |
| Thu, 15 Mar 2012 22:08:53 +0100 | wenzelm | declare command keywords via theory header, including strict checking outside Pure; | file | diff | annotate |
| Thu, 29 Dec 2011 18:54:07 +0100 | huffman | remove constant 'ccpo.lub', re-use constant 'Sup' instead | file | diff | annotate |