equal
deleted
inserted
replaced
4 set ThyOutput.source; |
4 set ThyOutput.source; |
5 use "../../antiquote_setup.ML"; |
5 use "../../antiquote_setup.ML"; |
6 |
6 |
7 use_thy "Introduction"; |
7 use_thy "Introduction"; |
8 use_thy "Outer_Syntax"; |
8 use_thy "Outer_Syntax"; |
|
9 use_thy "Document_Preparation"; |
9 use_thy "Spec"; |
10 use_thy "Spec"; |
10 use_thy "Proof"; |
11 use_thy "Proof"; |
11 use_thy "Document_Preparation"; |
|
12 use_thy "Misc"; |
12 use_thy "Misc"; |
13 use_thy "Generic"; |
13 use_thy "Generic"; |
14 use_thy "HOL_Specific"; |
14 use_thy "HOL_Specific"; |
15 use_thy "Quick_Reference"; |
15 use_thy "Quick_Reference"; |
16 use_thy "ML_Tactic"; |
16 use_thy "ML_Tactic"; |