| author | wenzelm |
| Thu, 03 Mar 2016 21:59:21 +0100 | |
| changeset 62508 | d0b68218ea55 |
| parent 62387 | src/Pure/RAW/fixed_int_dummy.ML@ad3eb2889f9a |
| permissions | -rw-r--r-- |
|
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62387
diff
changeset
|
1 |
(* Title: Pure/ML/fixed_int_dummy.ML |
|
62387
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
diff
changeset
|
2 |
|
|
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
diff
changeset
|
3 |
FixedInt dummy that is not fixed (up to Poly/ML 5.6). |
|
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
diff
changeset
|
4 |
*) |
|
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
diff
changeset
|
5 |
|
|
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
diff
changeset
|
6 |
structure FixedInt = IntInf; |