author | wenzelm |
Mon, 19 Oct 2009 23:02:56 +0200 | |
changeset 33004 | 715566791eb0 |
parent 23452 | 95b70054bb3a |
child 33037 | b22e44496dc2 |
permissions | -rw-r--r-- |
23452 | 1 |
(* Metis-specific ML environment *) |
2 |
nonfix ++ -- RL mem union subset; |
|
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 |