]> matita.cs.unibo.it Git - helm.git/blobdiff - weblib/tutorial/chapter1.ma
commit by user andrea
[helm.git] / 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