author | haftmann |
Wed, 05 May 2010 18:25:34 +0200 | |
changeset 36692 | 54b64d4ad524 |
parent 33037 | b22e44496dc2 |
permissions | -rw-r--r-- |
23452 | 1 |
(* Metis-specific ML environment *) |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
33037
diff
changeset
|
2 |
nonfix ++ -- RL; |
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 |