| Thu, 15 Sep 2005 08:16:22 +0200 | haftmann | fixed type annotation | file | diff | annotate |
| Wed, 14 Sep 2005 23:00:03 +0200 | chaieb | Unfortunately patched to use IntInf.int instead of just int (SML compatibility) | 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 |