]> matita.cs.unibo.it Git - helm.git/commitdiff
commit by user andrea
authormatitaweb <claudio.sacerdoticoen@unibo.it>
Wed, 7 Mar 2012 10:37:08 +0000 (10:37 +0000)
committermatitaweb <claudio.sacerdoticoen@unibo.it>
Wed, 7 Mar 2012 10:37:08 +0000 (10:37 +0000)
weblib/tutorial/chapter2.ma

index 7260a33aff9d5ef96b975289df80d1dbe2c675f8..e3dfd1d4470a8bac423d9177f25e9b5b9d9ec49d 100644 (file)
@@ -231,7 +231,8 @@ lemma div2_ok: ∀n,q,r. \ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"
     ]
 qed.
 
-(* \ 5h2 class="section"\ 6Mixing proofs and computations\ 5/h2\ 6
+(* 
+\ 5h2 class="section"\ 6Mixing proofs and computations\ 5/h2\ 6
 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