--- a/src/Pure/library.ML Sat Sep 03 22:27:06 2005 +0200
+++ b/src/Pure/library.ML Mon Sep 05 08:14:35 2005 +0200
@@ -8,14 +8,13 @@
tables, balanced trees, orders, current directory, misc.
*)
-infix |> |-> ||> ||>> |>> |>>> #> #-> ~~ \ \\ ins ins_string ins_int
- orf andf prefix upto downto mem mem_int mem_string union union_int
- union_string inter inter_int inter_string subset subset_int
- subset_string;
+infix 1 |> |-> ||> ||>> |>> |>>> #> #->;
+infix 2 ?;
+infix 3 o oo ooo oooo;
-infix 2 ?;
-
-infix 3 oo ooo oooo;
+infix 4 ~~ upto downto;
+infix orf andf prefix \ \\ ins ins_string ins_int mem mem_int mem_string union union_int
+ union_string inter inter_int inter_string subset subset_int subset_string;
signature BASIC_LIBRARY =
sig