X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fsubstitution.ma;h=0c9b86b0057df354d08c636b07b0c2a9d1086f8d;hb=026c6c5b0e094b2e6e8244909bc5ac3d88b70b9c;hp=c4335ca3e313a15b55615084f12daa3f54a6a20c;hpb=f1f445457c73202fd696c1b9fe0b24c0bafe2452;p=helm.git

diff --git a/helm/software/matita/library/didactic/exercises/substitution.ma b/helm/software/matita/library/didactic/exercises/substitution.ma
index c4335ca3e..0c9b86b00 100644
--- a/helm/software/matita/library/didactic/exercises/substitution.ma
+++ b/helm/software/matita/library/didactic/exercises/substitution.ma
@@ -1,17 +1,3 @@
-(* Esercitazione di logica 22/10/2008. *)
-
-(* Nota per gli studenti
-   =====================
-
-   * La lezione del pomeriggio con il Prof. Sacerdoti si terrà in aula 
-     Pinkerle e non Cremona.
-
-   * Un piccolo manuale sul software Matita è disponibile al seguente URL:
-
-       http://mowgli.cs.unibo.it/~tassi/exercise-induction.ma.html 
-
-*)
-   
 (* Esercizio 0 
    ===========
    
@@ -246,7 +232,9 @@ definition v1101 ≝ λx.
 definition esempio1 ≝ 
   (FImpl (FNot (FAtom 3)) (FOr (FAtom 2) (FAnd (FAtom 1) (FAtom 0)))).
 
-eval normalize on [[ esempio1 ]]_v1101.
+(* Decommenta ed esegui. *)
+
+(* eval normalize on [[ esempio1 ]]_v1101. *)
 
 
 (* Esercizio 3
@@ -317,7 +305,9 @@ definition esempio2 ≝ (FAnd (FImpl (FAtom 2) (FAtom 1)) (FAtom 2)).
    
 definition esempio3 ≝ (FOr (FAtom 0) (FAtom 1)).
 
-eval normalize on (esempio2 [ esempio3 / 2]).
+(* Decommenta ed esegui *)
+
+(* eval normalize on (esempio2 [ esempio3 / 2]). *)
 
 (*DOCBEGIN