# HG changeset patch # User nipkow # Date 759423584 -3600 # Node ID c1a3020635a1dbbded3fc95bc12d36cb238e9152 # Parent 7d437bed77658325fce2e8d6ef3c8c47b2a11736 added qsort diff -r 7d437bed7765 -r c1a3020635a1 ex/ROOT.ML --- a/ex/ROOT.ML Mon Jan 24 15:59:02 1994 +0100 +++ b/ex/ROOT.ML Mon Jan 24 15:59:44 1994 +0100 @@ -13,6 +13,7 @@ time_use "ex/cla.ML"; time_use "ex/meson.ML"; time_use "ex/mesontest.ML"; +time_use_thy "ex/Qsort"; time_use_thy "ex/LexProd"; time_use_thy "ex/Puzzle"; time_use "ex/set.ML";