From 625846fd7d1b0063b3b3a81ff9bbf36ddccf84f1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 21 Oct 2008 14:50:59 +0000 Subject: [PATCH] ... --- helm/software/matita/contribs/didactic/Makefile | 2 +- .../matita/contribs/didactic/induction.ma | 17 ++++++++++++++++- 2 files changed, 17 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/contribs/didactic/Makefile b/helm/software/matita/contribs/didactic/Makefile index 212f1055b..d31ab5525 100644 --- a/helm/software/matita/contribs/didactic/Makefile +++ b/helm/software/matita/contribs/didactic/Makefile @@ -17,6 +17,6 @@ depend.opt: exercise-%: % cp $< $@ perl -ne 'undef $$/;s/\(\*BEGIN.*?END\*\)/…/msg;print' -i $@ - #perl -ne 'undef $$/;s/\(\*DOCBEGIN.*?DOCEND\*\)//msg;print' -i $@ + perl -ne 'undef $$/;s/\(\*DOCBEGIN.*?DOCEND\*\)//msg;print' -i $@ (echo ''; awk 'BEGIN { p = 0; } /DOCEND/ { p = 0; } { if (p == 1) print $$0; } /DOCBEGIN/ { p = 1;}' < $< | markdown; echo '') > $@.html diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma index 2296666c7..e2da2243a 100644 --- 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 -- 2.39.2