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

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma
index c8359a5498a3a4835ca0907358437411de7ab888..c87433c2dab5515fab805d4a0839cf2155a621d1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma
@@ -16,7 +16,7 @@ include "basic_2/notation/relations/btsn_5.ma".
 include "basic_2/reduction/fpb.ma".
 include "basic_2/computation/csx.ma".
 
-(* "QRST" STRONGLY NORMALIZING TERMS ****************************************)
+(* "QRST" STRONGLY NORMALIZING CLOSURES *************************************)
 
 inductive fsb (h) (g): relation3 genv lenv term ≝
 | fsb_intro: ∀G1,L1,T1. (