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

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

diff --git a/matita/matita/lib/basics/deqsets.ma b/matita/matita/lib/basics/deqsets.ma
index 2d6434f6578ffc2f4440aa5843388068be8e22ba..e874eb8ffe6487fd9cd5bc7489c3ed375030ffc3 100644 (file)
--- a/matita/matita/lib/basics/deqsets.ma
+++ b/matita/matita/lib/basics/deqsets.ma
@@ -28,6 +28,10 @@ notation "\P H" non associative with precedence 90
 notation "\b H" non associative with precedence 90 
   for @{(proj2 … (eqb_true ???) $H)}. 
   
+notation < "𝐃" non associative with precedence 90 
+ for @{'bigD}.
+interpretation "DeqSet" 'bigD = (mk_DeqSet ???).
+  
 lemma eqb_false: ∀S:DeqSet.∀a,b:S. 
   (eqb ? a b) = false ↔ a ≠ b.
 #S #a #b % #H