src/HOL/MicroJava/JVM/JVMListExample.thy
changeset 24783 5a3e336a2e37
parent 24340 811f78424efc
child 28408 e26aac53723d
equal deleted inserted replaced
24782:38e5c05ef741 24783:5a3e336a2e37
    89 
    89 
    90 types_code
    90 types_code
    91   cnam ("string")
    91   cnam ("string")
    92   vnam ("string")
    92   vnam ("string")
    93   mname ("string")
    93   mname ("string")
    94   loc_ ("int")
    94   loc' ("int")
    95 
    95 
    96 consts_code
    96 consts_code
    97   "new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
    97   "new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
    98 attach {*
    98 attach {*
    99 fun new_addr p none loc hp =
    99 fun new_addr p none loc hp =