| changeset 24051 | 896fb015079c |
| parent 16417 | 9bc16273c2d4 |
| child 24892 | c663e675e177 |
--- a/src/ZF/UNITY/AllocImpl.thy Sun Jul 29 14:30:06 2007 +0200 +++ b/src/ZF/UNITY/AllocImpl.thy Sun Jul 29 14:30:07 2007 +0200 @@ -69,10 +69,7 @@ declare alloc_prog_def [THEN def_prg_Init, simp] declare alloc_prog_def [THEN def_prg_AllowedActs, simp] -ML -{* -program_defs_ref := [thm"alloc_prog_def"] -*} +declare alloc_prog_def [program] declare alloc_giv_act_def [THEN def_act_simp, simp] declare alloc_rel_act_def [THEN def_act_simp, simp]