src/ZF/ex/ParContract.ML
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));