set quick_and_dirty;+− +− use_thy "Intro";+− use_thy "FirstSteps";+− use_thy "Parsing";+− use_thy "NamedThms";+− use_thy "Transformation";+−