diff -r 8d06e11a01d1 -r fbdfceb8de15 src/HOL/MicroJava/BV/JType.thy --- a/src/HOL/MicroJava/BV/JType.thy Fri Nov 09 19:37:30 2007 +0100 +++ b/src/HOL/MicroJava/BV/JType.thy Fri Nov 09 19:37:32 2007 +0100 @@ -6,7 +6,7 @@ header {* \isaheader{The Java Type System as Semilattice} *} -theory JType imports WellForm Err begin +theory JType imports "../J/WellForm" Err begin constdefs super :: "'a prog \ cname \ cname"