src/Pure/ML/fixed_int_dummy.ML
author wenzelm
Fri, 18 Mar 2016 17:58:19 +0100
changeset 62668 360d3464919c
parent 62508 d0b68218ea55
permissions -rw-r--r--
discontinued slightly odd "secure" mode;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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;