X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale_tests%2Fmicro_tests3.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale_tests%2Fmicro_tests3.ma;h=71bd37984ff8c2b55ee17769f7e04b3cfbd3fb74;hb=e3fc33cab9b7736c6475cf2c9cd7f91c5a4bd7f9;hp=c6d6390d511a08a30cd6eff8e8ace55e41b998c8;hpb=a7e36d2d1da42fb17a2a6c1c737bddc90b2d3040;p=helm.git diff --git a/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests3.ma b/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests3.ma index c6d6390d5..71bd37984 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests3.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests3.ma @@ -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.