...

[helm.git] / helm / software / matita / library / didactic / exercises / duality.ma

diff --git a/helm/software/matita/library/didactic/exercises/duality.ma b/helm/software/matita/library/didactic/exercises/duality.ma
index c04859bd142ea693521ba637ba6c017e979c5516..dca98ddc7652616d5e2f9a63977e28f061bd3e19 100644 (file)
--- a/helm/software/matita/library/didactic/exercises/duality.ma
+++ b/helm/software/matita/library/didactic/exercises/duality.ma
@@ -1,11 +1,3 @@
-(* Esercitazione di logica 29/10/2008. 
-
-   Note per gli esercizi: 
-   
-     http://www.cs.unibo.it/~tassi/exercise-duality.ma.html
-
-*)
-
 (* Esercizio 0
    ===========
 
@@ -138,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
 
@@ -196,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
    ==========
@@ -247,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
    ===========