| Thu, 08 Jun 2006 14:48:28 +0200 | nipkow | less_equal -> less_eq (someone had screwd up here) | file | diff | annotate |
| Fri, 17 Mar 2006 09:34:23 +0100 | haftmann | renamed op < <= to Orderings.less(_eq) | file | diff | annotate |
| Fri, 10 Mar 2006 15:33:48 +0100 | haftmann | renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc. | file | diff | annotate |
| Tue, 20 Sep 2005 16:17:34 +0200 | haftmann | introduced AList module in favor of assoc etc. | file | diff | annotate |
| Thu, 15 Sep 2005 22:16:23 +0200 | chaieb | The SMLNJ Problem fixed... | file | diff | annotate |
| Wed, 14 Sep 2005 17:25:52 +0200 | chaieb | The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy | file | diff | annotate |