| changeset 55601 | b7f4da504b75 |
| parent 55600 | 3c7610b8dcfc |
| child 55602 | 257bd115fcca |
| 55600:3c7610b8dcfc | 55601:b7f4da504b75 |
|---|---|
1 (* Title: HOL/ex/Interpretation_with_Defs.thy |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* Interpretation accompanied with mixin definitions. EXPERIMENTAL. *} |
|
6 |
|
7 theory Interpretation_with_Defs |
|
8 imports Pure |
|
9 keywords "defining" and "permanent_interpretation" :: thy_goal |
|
10 begin |
|
11 |
|
12 ML_file "~~/src/Tools/interpretation_with_defs.ML" |
|
13 |
|
14 end |