- grafiteParser: we added the comand "defined" as a presentational

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / fsb_aaa.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma
index 6dff4c048ee6a71d1b55a33a92bd2aa33ca2cfeb..5a8d5d2408d9beee1b0d2191349b82e52982cf5d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma
@@ -16,7 +16,7 @@ include "basic_2/computation/fpbs_aaa.ma".
 include "basic_2/computation/csx_aaa.ma".
 include "basic_2/computation/fsb_csx.ma".
 
-(* "QRST" STRONGLY NORMALIZING TERMS ****************************************)
+(* "QRST" STRONGLY NORMALIZING CLOSURES *************************************)
 
 (* Main properties **********************************************************)