Added a turing/universal directory for the universal turing machine (and

[helm.git] / matita / matita / lib / basics / finset.ma

diff --git a/matita/matita/lib/basics/finset.ma b/matita/matita/lib/basics/finset.ma
index 3efd26f3f59fcb806a7f795371ba3539a9f7905b..a8ee13a074ad558fbd733c1f2b7718a9d0177c96 100644 (file)
--- a/matita/matita/lib/basics/finset.ma
+++ b/matita/matita/lib/basics/finset.ma
@@ -19,6 +19,10 @@ record FinSet : Type[1] ≝
   enum_unique: uniqueb FinSetcarr enum = true
 }.
 
+notation < "𝐅" non associative with precedence 90 
+ for @{'bigF}.
+interpretation "FinSet" 'bigF = (mk_FinSet ???).
+
 (* bool *)
 lemma bool_enum_unique: uniqueb ? [true;false] = true.
 // qed.