decentralizing core notation

[helm.git] / matita / matita / lib / turing / wmono.ma

diff --git a/matita/matita/lib/turing/wmono.ma b/matita/matita/lib/turing/wmono.ma
index 35c409639a7dfbc60f1a5f43829e7bb73370c2a9..d31ed62f551dabdb8e2963041c664f7b64e30415 100644 (file)
--- a/matita/matita/lib/turing/wmono.ma
+++ b/matita/matita/lib/turing/wmono.ma
@@ -11,6 +11,7 @@
 
 include "basics/vectors.ma".
 include "basics/finset.ma".
+include "basics/core_notation/compose_2.ma".
 (* include "basics/relations.ma". *)
 
 record tape (sig:FinSet): Type[0] ≝