| changeset 42463 | f270e3e18be5 |
| parent 35440 | bdf8ad377877 |
| child 46720 | 9722171731af |
--- a/src/HOL/MicroJava/BV/Effect.thy Fri Apr 22 15:57:43 2011 +0200 +++ b/src/HOL/MicroJava/BV/Effect.thy Sat Apr 23 13:00:19 2011 +0200 @@ -9,8 +9,7 @@ imports JVMType "../JVM/JVMExceptions" begin -types - succ_type = "(p_count \<times> state_type option) list" +type_synonym succ_type = "(p_count \<times> state_type option) list" text {* Program counter of successor instructions: *} primrec succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count list" where