changeset 41589 | bbd861837ebc |
parent 16417 | 9bc16273c2d4 |
child 46783 | 3e89a5cab8d7 |
41588:9546828c0eb3 | 41589:bbd861837ebc |
---|---|
1 (* Title: HOL/Import/HOL/HOL4.thy |
1 (* Title: HOL/Import/HOL/HOL4.thy |
2 ID: $Id$ |
2 Author: Sebastian Skalberg, TU Muenchen |
3 Author: Sebastian Skalberg (TU Muenchen) |
|
4 *) |
3 *) |
5 |
4 |
6 theory HOL4 imports HOL4Vec HOL4Word32 HOL4Real begin |
5 theory HOL4 imports HOL4Vec HOL4Word32 HOL4Real begin |
7 |
6 |
8 end |
7 end |