changeset 15481 | fc075ae929e4 |
parent 13717 | 78f91fcdf560 |
child 17088 | 3f797ec16f02 |
--- a/src/HOL/MicroJava/BV/Effect.thy Sun Jan 30 20:48:50 2005 +0100 +++ b/src/HOL/MicroJava/BV/Effect.thy Tue Feb 01 18:01:57 2005 +0100 @@ -6,7 +6,10 @@ header {* \isaheader{Effect of Instructions on the State Type} *} -theory Effect = JVMType + JVMExceptions: +theory Effect +imports JVMType "../JVM/JVMExceptions" +begin + types succ_type = "(p_count \<times> state_type option) list"