From 24ef33f1fde3be06cfce603e8437cde48dbf214d Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 7 Mar 2012 08:46:44 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter10.ma | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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. - -- 2.39.2