]> matita.cs.unibo.it Git - helm.git/commitdiff
commit by user andrea
authormatitaweb <claudio.sacerdoticoen@unibo.it>
Sat, 5 Nov 2011 16:56:56 +0000 (16:56 +0000)
committermatitaweb <claudio.sacerdoticoen@unibo.it>
Sat, 5 Nov 2011 16:56:56 +0000 (16:56 +0000)
weblib/tutorial/chapter1.ma

index 5da976a523cbfd08ef18f9967a1a871d488e8b9e..b21fd3e1787add792e06acdb24dbf62c14dba2b0 100644 (file)
@@ -149,7 +149,8 @@ inductive opp : \ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"\ 6bank\ 5/a\ 6
 (* In precisely the same way as "bank" is the smallest type containing east and
 west, opp is the smallest predicate containing the two sub-cases east_west and
 weast_east. If you have some familiarity with Prolog, you may look at opp as the
-predicate definined by the two clauses - in this case, the two facts -
+predicate defined by the two clauses - in this case, the two facts - ast_west and
+west_east.
 
 Between opp and opposite we have the following relation:
     opp a b iff a = opposite b