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

index 24efb3e983e9f6986be23ed8055d09df08388b51..bfdf8016c82ee47d0a9e2b3adf7e204d7028073a 100644 (file)
@@ -1,5 +1,5 @@
 (* 
-\ 5h1\ 6Equivalence\ 5/h1\ 6*)
+\ 5h1\ 6Regular Expressions Equivalence\ 5/h1\ 6*)
 
 include "tutorial/chapter9.ma".
 
@@ -395,4 +395,3 @@ definition exp9 ≝ (\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6\ 5a t
 example ex1 : \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter10/equiv.def(9)"\ 6equiv\ 5/a\ 6 ? (\ 5a href="cic:/matita/tutorial/chapter10/exp8.def(10)"\ 6exp8\ 5/a\ 6\ 5a title="re or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/exp9.def(10)"\ 6exp9\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/exp9.def(10)"\ 6exp9\ 5/a\ 6\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
 normalize // qed.
 
-