]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
WIP in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / bdd_term.ma
index 8d514e0d7f2a1fe8ff3438166b9aed1388d93d9c..9cfe28ad9dc81a650ab98325739f00674f75af20 100644 (file)
@@ -35,7 +35,7 @@ interpretation
   "by-depth delayed (prototerm)"
   'ClassDPhi = (bdd).
 
-(*
+(* COMMENT
 
 (* Basic inversions *********************************************************)
 
@@ -213,4 +213,4 @@ lemma bbd_mono_in_root_d:
   ]
 ]
 qed-.
-*)
\ No newline at end of file
+*)