1 quick_and_dirty := true;
2
3 use_thys [
4 "Introduction",
5 "Framework",
6 "First_Order_Logic",
7 "Outer_Syntax",
8 "Document_Preparation",
9 "Spec",
10 "Proof",
11 "Inner_Syntax",
12 "Misc",
13 "Generic",
14 "HOL_Specific",
15 "Quick_Reference",
16 "Symbols",
17 "ML_Tactic"
18 ];