Mon, 11 Jun 2007 11:06:15 +0200 | chaieb | tuned tactic | changeset | files |
Mon, 11 Jun 2007 11:06:13 +0200 | chaieb | Temporarily use int instead of IntInf.int but Code generator should map HOL's int to ML's IntInf.int --- To be fixed | changeset | files |