]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/lib/re/moves.ma
- notation (possibly affecting all .ma files):
[helm.git] / matita / matita / lib / re / moves.ma
index 1372b49760ee677eea226d73a3a70392bc869e86..5825317771ee6f5672b92d25cd97713166d048bd 100644 (file)
@@ -110,7 +110,7 @@ theorem move_ok:
   ]
 qed.
     
-notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
+notation > "x ↦* E" non associative with precedence 65 for @{moves ? $x $E}.
 let rec moves (S : DeqSet) w e on w : pre S ≝
  match w with
   [ nil ⇒ e