equal
deleted
inserted
replaced
1 |
1 set quick_and_dirty; |
2 (* $Id$ *) |
|
3 |
|
4 set ThyOutput.source; |
2 set ThyOutput.source; |
5 use "../../antiquote_setup.ML"; |
3 use "../../antiquote_setup.ML"; |
6 |
4 |
7 use_thy "Introduction"; |
5 use_thys [ |
8 use_thy "Outer_Syntax"; |
6 "Introduction", |
9 use_thy "Document_Preparation"; |
7 "Framework", |
10 use_thy "Spec"; |
8 "First_Order_Logic", |
11 use_thy "Proof"; |
9 "Outer_Syntax", |
12 use_thy "Inner_Syntax"; |
10 "Document_Preparation", |
13 use_thy "Misc"; |
11 "Spec", |
14 use_thy "Generic"; |
12 "Proof", |
15 use_thy "HOL_Specific"; |
13 "Inner_Syntax", |
16 use_thy "Quick_Reference"; |
14 "Misc", |
17 use_thy "Symbols"; |
15 "Generic", |
18 use_thy "ML_Tactic"; |
16 "HOL_Specific", |
|
17 "Quick_Reference", |
|
18 "Symbols", |
|
19 "ML_Tactic" |
|
20 ]; |