]> matita.cs.unibo.it Git - helm.git/commitdiff
qed => nqed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 26 Oct 2009 14:15:34 +0000 (14:15 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 26 Oct 2009 14:15:34 +0000 (14:15 +0000)
helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests3.ma

index c6d6390d511a08a30cd6eff8e8ace55e41b998c8..71bd37984ff8c2b55ee17769f7e04b3cfbd3fb74 100755 (executable)
@@ -73,4 +73,4 @@ nlemma ok_mTest_HCS08_ROL_ROR_full :
            (mTest_HCS08_ROL_ROR_status t) (mk_word16 〈x1,x8〉 〈x6,xC〉)).
  #t; nelim t;
  napply refl_eq.
-qed.
+nqed.