changeset 434 | 89d45187f04d |
parent 0 | a5a9c433f639 |
child 477 | 53fc8ad84b33 |
--- a/src/ZF/ex/ParContract.ML Tue Jun 21 11:55:36 1994 +0200 +++ b/src/ZF/ex/ParContract.ML Tue Jun 21 16:26:34 1994 +0200 @@ -22,7 +22,8 @@ val type_intrs = Comb.intrs@[SigmaI]; val type_elims = [SigmaE2]); -val [parcontract_refl,K_parcontract,S_parcontract,Ap_parcontract] = ParContract.intrs; +val [parcontract_refl,K_parcontract,S_parcontract,Ap_parcontract] = + ParContract.intrs; val parcontract_induct = standard (ParContract.mutual_induct RS spec RS spec RSN (2,rev_mp));