changeset 3841 | 22bbc1676768 |
parent 3840 | e0baea4d485a |
child 6044 | e0f9d930e956 |
--- a/src/ZF/ex/Primrec.thy Fri Oct 10 18:23:31 1997 +0200 +++ b/src/ZF/ex/Primrec.thy Fri Oct 10 18:37:49 1997 +0200 @@ -57,7 +57,7 @@ PREC "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec" monos "[list_mono]" con_defs "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]" - type_intrs "nat_typechecks @ list. intrs @ + type_intrs "nat_typechecks @ list.intrs @ [lam_type, list_case_type, drop_type, map_type, apply_type, rec_type]"