From: matitaweb Date: Wed, 7 Mar 2012 08:46:44 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~1888 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=24ef33f1fde3be06cfce603e8437cde48dbf214d commit by user andrea --- diff --git a/weblib/tutorial/chapter10.ma b/weblib/tutorial/chapter10.ma index 24efb3e98..bfdf8016c 100644 --- a/weblib/tutorial/chapter10.ma +++ b/weblib/tutorial/chapter10.ma @@ -1,5 +1,5 @@ (* -h1Equivalence/h1*) +h1Regular Expressions Equivalence/h1*) include "tutorial/chapter9.ma". @@ -395,4 +395,3 @@ definition exp9 ≝ (a href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa t example ex1 : a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter10/equiv.def(9)"equiv/a ? (a href="cic:/matita/tutorial/chapter10/exp8.def(10)"exp8/aa title="re or" href="cic:/fakeuri.def(1)"+/aa href="cic:/matita/tutorial/chapter10/exp9.def(10)"exp9/a) a href="cic:/matita/tutorial/chapter10/exp9.def(10)"exp9/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. normalize // qed. -