changeset 16417 | 9bc16273c2d4 |
parent 12951 | a9fdcb71d252 |
child 35102 | cc7a0b9f938c |
16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
---|---|
4 Copyright 1999 Technische Universitaet Muenchen |
4 Copyright 1999 Technische Universitaet Muenchen |
5 *) |
5 *) |
6 |
6 |
7 header {* \isaheader{Java types} *} |
7 header {* \isaheader{Java types} *} |
8 |
8 |
9 theory Type = JBasis: |
9 theory Type imports JBasis begin |
10 |
10 |
11 typedecl cnam |
11 typedecl cnam |
12 |
12 |
13 -- "exceptions" |
13 -- "exceptions" |
14 datatype |
14 datatype |