equal
deleted
inserted
replaced
4 Copyright 2000 TUM |
4 Copyright 2000 TUM |
5 *) |
5 *) |
6 |
6 |
7 header {* \isaheader{The Java Type System as Semilattice} *} |
7 header {* \isaheader{The Java Type System as Semilattice} *} |
8 |
8 |
9 theory JType imports WellForm Err begin |
9 theory JType imports "../J/WellForm" Err begin |
10 |
10 |
11 constdefs |
11 constdefs |
12 super :: "'a prog \<Rightarrow> cname \<Rightarrow> cname" |
12 super :: "'a prog \<Rightarrow> cname \<Rightarrow> cname" |
13 "super G C == fst (the (class G C))" |
13 "super G C == fst (the (class G C))" |
14 |
14 |