equal
deleted
inserted
replaced
1 (* Title: "BaseDefinitions/BaseDefinitions.thy" |
1 (* Title: "BaseDefinitions/BaseDefinitions.thy" |
2 Author: Walther Neuper 190823 |
2 Author: Walther Neuper 190823 |
3 (c) due to copyright terms |
3 (c) due to copyright terms |
4 |
4 |
5 KEStore holds Theory_Data (problems, methods, etc). |
5 KEStore holds Theory_Data (problems, methods, etc) and requires respective definitions. |
6 The directory BaseDefinitions/ holds definitions (in "*-def.sml") required for KEStore; |
|
7 many of these files have respective "*.sml" files with further code, |
|
8 located at appropriate positions in the code. |
|
9 *) |
6 *) |
10 theory BaseDefinitions imports KEStore |
7 theory BaseDefinitions imports KEStore |
11 begin |
8 begin |
12 ML_file termC.sml |
9 ML_file termC.sml |
13 ML_file contextC.sml |
10 ML_file contextC.sml |