From: matitaweb Date: Wed, 7 Mar 2012 10:37:08 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~1882 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=df544317f1496afa4ab356b0324d645a240d1dbf commit by user andrea --- 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