Notes.

diff --git a/matita/matita/lib/tutorial/chapter12.ma b/matita/matita/lib/tutorial/chapter12.ma
index 7923b2b26e07edaeddf7192eafac0e09fef6c5cc..c0d8f8ae8d186791a7b9d0a67688cc1e0fa614be 100644 (file)
--- 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? ####################### *)