models ported

[helm.git] / helm / software / matita / contribs / didactic / induction.ma

diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma
index aa7b7aff6d7a742d4ac5359bb34434c890b0ba64..e2da2243ac90ede12b9d3be50969659b8fd71481 100644 (file)
--- a/helm/software/matita/contribs/didactic/induction.ma
+++ b/helm/software/matita/contribs/didactic/induction.ma
@@ -1,4 +1,16 @@
 (* 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 
    ===========
@@ -21,7 +33,10 @@
    
    * salvare il file (menu `File ▹ Save as ...`) nella directory (cartella)
      /public/ con nome linguaggi_Account1.ma, ad esempio Mario Rossi, il cui
-     account è mrossi deve salvare il file in /public/linguaggi_mrossi.ma
+     account è mrossi, deve salvare il file in /public/linguaggi_mrossi.ma
+
+   * mandatevi via email o stampate il file. Per stampare potete usare
+     usare l'editor gedit che offre la funzionalità di stampa
 *)
 
 (*DOCBEGIN
@@ -190,7 +205,7 @@ let rec sem (v: nat → nat) (F: Formula) on F ≝
 *)
 definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
 notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 90 for @{ 'if_then_else $e $t $f }.
-notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 90 for @{ 'if_then_else _ $e $t $f }.
+notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 90 for @{ 'if_then_else $e $t $f }.
 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f).
 notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
 notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.