equal
deleted
inserted
replaced
1 (* Title: HOLCF/thy_syntax.ML |
1 (* Title: HOLCF/thy_syntax.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Mayr |
3 Author: Tobias Mayr |
4 |
4 |
5 Installation of the additional theory file sections for HOLCF: axioms , ops |
5 Additional thy file sections for HOLCF: axioms, ops. |
6 There's an elaborate but german description of this extension |
|
7 and a short english description of the new sections, |
|
8 write to mayrt@informatik.tu-muenchen.de. |
|
9 |
|
10 TODO: |
|
11 |
|
12 *) |
6 *) |
13 |
7 |
14 (* use "holcflogics.ML"; |
8 (* use "holcflogics.ML"; |
15 use "thy_axioms.ML"; |
9 use "thy_axioms.ML"; |
16 use "thy_ops.ML"; should already have been done in ROOT.ML *) |
10 use "thy_ops.ML"; should already have been done in ROOT.ML *) |