src/Tools/WWW_Find/ROOT.ML
changeset 48722 a5e3ba7cbb2a
parent 48721 866f6d5baf4c
child 48723 0829e958f0aa
equal deleted inserted replaced
48721:866f6d5baf4c 48722:a5e3ba7cbb2a
     1 if ML_System.is_polyml then use_thy "WWW_Find"
       
     2 else ();
       
     3