| changeset 15481 | fc075ae929e4 |
| parent 14981 | e73f8140af78 |
| child 35416 | d8d7d1b785af |
--- a/src/HOL/MicroJava/Comp/DefsComp.thy Sun Jan 30 20:48:50 2005 +0100 +++ b/src/HOL/MicroJava/Comp/DefsComp.thy Tue Feb 01 18:01:57 2005 +0100 @@ -5,8 +5,9 @@ (* Definitions for accessing parts of methods, states etc. *) -theory DefsComp = JVMExec: - +theory DefsComp +imports "../JVM/JVMExec" +begin constdefs