From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 29 Aug 2014 16:02:03 +0000 (+0000)
Subject: Notes.
X-Git-Tag: make_still_working~854
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=47079f99d6e48c735dec6b30f47a5f8c238bdab5

Notes.
---

diff --git a/matita/matita/lib/tutorial/chapter12.ma b/matita/matita/lib/tutorial/chapter12.ma
index 7923b2b26..c0d8f8ae8 100644
--- a/matita/matita/lib/tutorial/chapter12.ma
+++ b/matita/matita/lib/tutorial/chapter12.ma
@@ -631,6 +631,15 @@ theorem div_trace_to_diverging_trace':
  | #n #s #EQ destruct lapply (div_well_formed d n) /2 by div_well_formed, next_step/ ]
 qed.
 
+(* AGGIUNGERE SPIEGAZIONE SU PRODUTTIVITA' *)
+
+(* AGGIUNGERE SPIEGAZIONE SU CONFRONTO VALORI COINDUTTIVI *)
+
+(* AGGIUNGERE CONFRONTO CON TEORIA DELLE CATEGORIE *)
+
+(* AGGIUNGERE ESEMPI DI SEMANTICA OPERAZIONE BIG STEP PER LA DIVERGENZA;
+   DI PROPRIETA' DI SAFETY;
+   DI TOPOLOGIE COINDUTTIVAMENTE GENERATE? *)
 
 (* ################## COME SPIEGARLO QUI? ####################### *)