src/ZF/ex/Primrec.thy
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]"