X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter2.ma;h=2942d61524b941cc00daa7c6e59adb49bf974416;hb=dae100deb1f762fcff3978fe1cde87508192ca48;hp=7260a33aff9d5ef96b975289df80d1dbe2c675f8;hpb=f4a04a5af0748535ad7522c2a95dd3ae4344eac7;p=helm.git

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index 7260a33af..2942d6152 100644
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -1,4 +1,6 @@
+(*
 h1 class="section"Induction and Recursion/h1
+*)
 include "basics/types.ma".
 
 (* Most of the types we have seen so far are enumerated types, composed by a 
@@ -231,7 +233,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 
@@ -281,4 +284,4 @@ example quotient7: a href="cic:/matita/tutorial/chapter2/witness.fix(0,2,1)"wi
 example quotient8: a href="cic:/matita/tutorial/chapter2/witness.fix(0,2,1)"witness/a … (a href="cic:/matita/tutorial/chapter2/div2Pagain.def(4)"div2Pagain/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a)))))) 
        a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a))), a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉.
 // qed. 
-prepre /pre/pre
\ No newline at end of file
+prepre /pre/pre