X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter2.ma;fp=weblib%2Ftutorial%2Fchapter2.ma;h=e3dfd1d4470a8bac423d9177f25e9b5b9d9ec49d;hb=df544317f1496afa4ab356b0324d645a240d1dbf;hp=7260a33aff9d5ef96b975289df80d1dbe2c675f8;hpb=111e641bb0772a542293b796c9d4a18fc9d58a00;p=helm.git

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index 7260a33af..e3dfd1d44 100644
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -231,7 +231,8 @@ lemma div2_ok: ∀n,q,r. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"
     ]
 qed.
 
-(* h2 class="section"Mixing proofs and computations/h2
+(* 
+h2 class="section"Mixing proofs and computations/h2
 There is still another possibility, however, namely to mix the program and its 
 specification into a single entity. The idea is to refine the output type of the 
 div2 function: it should not be just a generic pair 〈q,r〉 of natural numbers but a