--- a/src/ZF/ex/ListN.thy Fri Oct 10 18:23:31 1997 +0200
+++ b/src/ZF/ex/ListN.thy Fri Oct 10 18:37:49 1997 +0200
@@ -16,5 +16,5 @@
intrs
NilI "<0,Nil> : listn(A)"
ConsI "[| a: A; <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"
- type_intrs "nat_typechecks @ list. intrs"
+ type_intrs "nat_typechecks @ list.intrs"
end
--- 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]"
--- a/src/ZF/ex/Rmap.thy Fri Oct 10 18:23:31 1997 +0200
+++ b/src/ZF/ex/Rmap.thy Fri Oct 10 18:37:49 1997 +0200
@@ -19,7 +19,7 @@
ConsI "[| <x,y>: r; <xs,ys> : rmap(r) |] ==>
<Cons(x,xs), Cons(y,ys)> : rmap(r)"
- type_intrs "[domainI,rangeI] @ list. intrs"
+ type_intrs "[domainI,rangeI] @ list.intrs"
end