src/Pure/library.ML
changeset 17257 0ab67cb765da
parent 17153 d871853e13e0
child 17313 7d97f60293ae
     1.1 --- a/src/Pure/library.ML	Sat Sep 03 22:27:06 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Mon Sep 05 08:14:35 2005 +0200
     1.3 @@ -8,14 +8,13 @@
     1.4  tables, balanced trees, orders, current directory, misc.
     1.5  *)
     1.6  
     1.7 -infix |> |-> ||> ||>> |>> |>>> #> #-> ~~ \ \\ ins ins_string ins_int
     1.8 -  orf andf prefix upto downto mem mem_int mem_string union union_int
     1.9 -  union_string inter inter_int inter_string subset subset_int
    1.10 -  subset_string;
    1.11 +infix 1 |> |-> ||> ||>> |>> |>>> #> #->;
    1.12 +infix 2 ?;
    1.13 +infix 3 o oo ooo oooo;
    1.14  
    1.15 -infix 2 ?;
    1.16 -
    1.17 -infix 3 oo ooo oooo;
    1.18 +infix 4 ~~ upto downto;
    1.19 +infix orf andf prefix \ \\ ins ins_string ins_int mem mem_int mem_string union union_int
    1.20 +  union_string inter inter_int inter_string subset subset_int subset_string;
    1.21  
    1.22  signature BASIC_LIBRARY =
    1.23  sig