equal
deleted
inserted
replaced
1 (* tactics, tacticals etc. for scripts |
1 (* Title: tactics, tacticals etc. for scripts |
2 W.N.24.2.00 |
2 Author: Walther Neuper 000224 |
3 use_thy_only"Scripts/Script"; |
3 (c) due to copyright terms |
4 use_thy"../Scripts/Script"; |
4 |
5 use_thy"Script"; |
5 use_thy_only"Scripts/Script"; |
|
6 use_thy"../Scripts/Script"; |
|
7 use_thy"Script"; |
6 *) |
8 *) |
7 |
9 |
8 theory Script |
10 theory Script imports Tools begin |
9 imports Tools |
|
10 begin |
|
11 |
11 |
12 typedecl |
12 typedecl |
13 ID (* identifiers for thy, ruleset,... *) |
13 ID (* identifiers for thy, ruleset,... *) |
14 |
14 |
15 typedecl |
15 typedecl |