changeset 71 | 729fe026c5f3 |
parent 16 | 0b033d50ca1c |
--- a/src/ZF/ex/prop.ML Fri Oct 22 11:34:41 1993 +0100 +++ b/src/ZF/ex/prop.ML Fri Oct 22 11:42:02 1993 +0100 @@ -24,7 +24,7 @@ "n: nat ==> #n : prop", "[| p: prop; q: prop |] ==> p=>q : prop"]; val monos = []; - val type_intrs = data_typechecks; + val type_intrs = datatype_intrs; val type_elims = []); val [FlsI,VarI,ImpI] = Prop.intrs;