src/HOL/Library/Library/ROOT.ML

added "no_assms" option to Refute, and include structured proof assumptions by default;
will do the same for Quickcheck unless there are objections

use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order"];