| changeset 32833 | f3716d1a2e48 |
| parent 30242 | aea5d7fa7ef5 |
| child 37216 | 3165bc303f66 |
| 32827:2729c8033326 | 32833:f3716d1a2e48 |
|---|---|
1 set quick_and_dirty; |
1 Unsynchronized.set quick_and_dirty; |
2 set ThyOutput.source; |
2 Unsynchronized.set ThyOutput.source; |
3 use "../../antiquote_setup.ML"; |
3 use "../../antiquote_setup.ML"; |
4 |
4 |
5 use_thys [ |
5 use_thys [ |
6 "Introduction", |
6 "Introduction", |
7 "Framework", |
7 "Framework", |