From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 16 Nov 2008 10:30:30 +0000 (+0000)
Subject: fixed
X-Git-Tag: make_still_working~4543
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1a506c25fe9952e1fee371f164d11837619dbac7;p=helm.git

fixed
---

diff --git a/helm/software/matita/library/didactic/exercises/duality.ma b/helm/software/matita/library/didactic/exercises/duality.ma
index ea3a987d3..dca98ddc7 100644
--- a/helm/software/matita/library/didactic/exercises/duality.ma
+++ b/helm/software/matita/library/didactic/exercises/duality.ma
@@ -130,8 +130,10 @@ definition v20 ≝ λx.
    La semantica della formula `(A ∨ C)` nel mondo `v20` in cui 
    `A` vale `2` e `C` vale `0` deve valere `1`.
    
+   Decommenta ed esegui.
 *)    
-eval normalize on [[FOr (FAtom 0) (FAtom 2)]]_v20. 
+
+(* eval normalize on [[FOr (FAtom 0) (FAtom 2)]]_v20. *) 
 
 (*DOCBEGIN
 
@@ -188,10 +190,12 @@ let rec negate (F: Formula) on F : Formula ≝
   
    Testare la funzione `negate`. Il risultato atteso è:
    
-       FOr (FNot (FAtom O)) (FImpl FTop (FNot (FAtom 1))) 
+       FOr (FNot (FAtom O)) (FImpl FTop (FNot (FAtom 1)))
+       
+   Decommenta ed esegui 
 *)
 
-eval normalize on (negate (FOr (FAtom 0) (FImpl FTop (FAtom 1)))).
+(* eval normalize on (negate (FOr (FAtom 0) (FImpl FTop (FAtom 1)))). *)
 
 (* ATTENZIONE
    ==========
@@ -239,9 +243,11 @@ let rec dualize (F : Formula) on F : Formula ≝
    Testare la funzione `dualize`. Il risultato atteso è:
    
        FAnd (FNot (FAtom O)) (FOr (FAtom 1) FTop) 
+       
+   Decommenta ed esegui.
 *)
 
-eval normalize on (dualize (FImpl (FAtom 0) (FAnd (FAtom 1) FBot))).
+(* eval normalize on (dualize (FImpl (FAtom 0) (FAnd (FAtom 1) FBot))). *)
 
 (* Spiegazione
    ===========
diff --git a/helm/software/matita/library/didactic/exercises/substitution.ma b/helm/software/matita/library/didactic/exercises/substitution.ma
index 096b5b84c..0c9b86b00 100644
--- a/helm/software/matita/library/didactic/exercises/substitution.ma
+++ b/helm/software/matita/library/didactic/exercises/substitution.ma
@@ -232,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
@@ -303,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