author | haftmann |
Thu, 29 Apr 2010 15:00:43 +0200 | |
changeset 36537 | b0186c66f324 |
parent 33037 | b22e44496dc2 |
child 36692 | 54b64d4ad524 |
permissions | -rw-r--r-- |
23452 | 1 |
(* Metis-specific ML environment *) |
33037
b22e44496dc2
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
haftmann
parents:
33004
diff
changeset
|
2 |
nonfix ++ -- RL mem; |
23452 | 3 |
val explode = String.explode; |
4 |
val implode = String.implode; |
|
5 |
val print = TextIO.print; |
|
33004
715566791eb0
always qualify NJ's old List.foldl/foldr in Isabelle/ML;
wenzelm
parents:
23452
diff
changeset
|
6 |
val foldl = List.foldl; |
715566791eb0
always qualify NJ's old List.foldl/foldr in Isabelle/ML;
wenzelm
parents:
23452
diff
changeset
|
7 |
val foldr = List.foldr; |
715566791eb0
always qualify NJ's old List.foldl/foldr in Isabelle/ML;
wenzelm
parents:
23452
diff
changeset
|
8 |