X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fopcodes%2FIP2022_instr_mode.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fopcodes%2FIP2022_instr_mode.ma;h=a12114d8036d86b2f6afaca82be6aad68413d470;hb=eb4144a401147a44a9620169eb6dafeb8f5a2c17;hp=45548e7b1250e6b79cc35cd7d0b35bb997b513f0;hpb=a79bf6edc13daaea8135ca71fdc92e02e229f030;p=helm.git diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode.ma index 45548e7b1..a12114d80 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode.ma @@ -68,7 +68,6 @@ ndefinition eq_IP2022_im ≝ | MODE_FR1n o1 ⇒ match i2 with [ MODE_FR1n o2 ⇒ eq_oct o1 o2 | _ ⇒ false ] ]. -(* iteratore sulle modalita' *) ndefinition forall_IP2022_im ≝ λP:IP2022_instr_mode → bool. P MODE_INH ⊗ forall_oct (λo.P (MODE_IMM3 o))