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