src/ZF/UNITY/AllocImpl.thy
changeset 24051 896fb015079c
parent 16417 9bc16273c2d4
child 24892 c663e675e177
     1.1 --- a/src/ZF/UNITY/AllocImpl.thy	Sun Jul 29 14:30:06 2007 +0200
     1.2 +++ b/src/ZF/UNITY/AllocImpl.thy	Sun Jul 29 14:30:07 2007 +0200
     1.3 @@ -69,10 +69,7 @@
     1.4  
     1.5  declare alloc_prog_def [THEN def_prg_Init, simp]
     1.6  declare alloc_prog_def [THEN def_prg_AllowedActs, simp]
     1.7 -ML
     1.8 -{*
     1.9 -program_defs_ref := [thm"alloc_prog_def"]
    1.10 -*}
    1.11 +declare alloc_prog_def [program]
    1.12  
    1.13  declare  alloc_giv_act_def [THEN def_act_simp, simp]
    1.14  declare  alloc_rel_act_def [THEN def_act_simp, simp]