| changeset 44035 | 322d1657c40c |
| parent 41589 | bbd861837ebc |
| child 45634 | b3dce535960f |
| 44034:53a081c8873d | 44035:322d1657c40c |
|---|---|
5 header {* |
5 header {* |
6 \chapter{Java Source Language}\label{cha:j} |
6 \chapter{Java Source Language}\label{cha:j} |
7 \isaheader{Some Auxiliary Definitions} |
7 \isaheader{Some Auxiliary Definitions} |
8 *} |
8 *} |
9 |
9 |
10 theory JBasis imports Main begin |
10 theory JBasis imports Main "~~/src/HOL/Library/Transitive_Closure_Table" begin |
11 |
11 |
12 lemmas [simp] = Let_def |
12 lemmas [simp] = Let_def |
13 |
13 |
14 section "unique" |
14 section "unique" |
15 |
15 |