src/ZF/ex/Primrec.thy
changeset 6117 f9aad8ccd590
parent 6044 e0f9d930e956
child 11316 b4e71bd751e4
     1.1 --- a/src/ZF/ex/Primrec.thy	Wed Jan 13 12:44:33 1999 +0100
     1.2 +++ b/src/ZF/ex/Primrec.thy	Wed Jan 13 15:14:47 1999 +0100
     1.3 @@ -26,8 +26,8 @@
     1.4      PROJ     "i: nat ==> PROJ(i) : prim_rec"
     1.5      COMP     "[| g: prim_rec; fs: list(prim_rec) |] ==> COMP(g,fs): prim_rec"
     1.6      PREC     "[| f: prim_rec; g: prim_rec |] ==> PREC(f,g): prim_rec"
     1.7 -  monos      "[list_mono]"
     1.8 -  con_defs   "[SC_def, CONST_def, PROJ_def, COMP_def, PREC_def]"
     1.9 +  monos       list_mono
    1.10 +  con_defs    SC_def, CONST_def, PROJ_def, COMP_def, PREC_def
    1.11    type_intrs "nat_typechecks @ list.intrs @                     
    1.12                [lam_type, list_case_type, drop_type, map_type,   
    1.13                apply_type, rec_type]"