equal
deleted
inserted
replaced
1 (* Title: HOL/MicroJava/J/SystemClasses.thy |
1 (* Title: HOL/MicroJava/J/SystemClasses.thy |
2 Author: Gerwin Klein |
2 Author: Gerwin Klein |
3 Copyright 2002 Technische Universitaet Muenchen |
3 Copyright 2002 Technische Universitaet Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* \isaheader{System Classes} *} |
6 section {* System Classes *} |
7 |
7 |
8 theory SystemClasses imports Decl begin |
8 theory SystemClasses imports Decl begin |
9 |
9 |
10 text {* |
10 text {* |
11 This theory provides definitions for the @{text Object} class, |
11 This theory provides definitions for the @{text Object} class, |