| Mon, 25 Jun 2007 12:16:27 +0200 | krauss | removed "sum_tools.ML" in favour of BalancedTree | file | diff | annotate |
| Sat, 02 Jun 2007 15:28:38 +0200 | krauss | "function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases. | file | diff | annotate |
| Thu, 10 May 2007 10:21:48 +0200 | haftmann | explicit import of Datatype.thy due to hook bootstrap problem | file | diff | annotate |
| Sun, 06 May 2007 21:49:23 +0200 | haftmann | tuned | file | diff | annotate |
| Thu, 26 Apr 2007 16:39:10 +0200 | wenzelm | added header; | file | diff | annotate |
| Tue, 10 Apr 2007 14:11:01 +0200 | krauss | Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now. | file | diff | annotate |
| Thu, 15 Feb 2007 17:35:19 +0100 | krauss | changed termination goal to use object quantifier | file | diff | annotate |