more robust parsing of TSTP sources -- Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
no_document use_thys [
"~~/src/HOL/Library/LaTeXsugar",
"~~/src/HOL/Library/OptionalSugar"
];
use_thy "Sugar";