(* *)
(* ********************************************************************** *)
-include "freescale/opcode_base_lemmas_opcode2.ma".
-include "freescale/opcode_base_lemmas_instrmode2.ma".
+include "freescale/opcode_base_lemmas_opcode.ma".
+include "freescale/opcode_base_lemmas_instrmode.ma".
include "num/word16_lemmas.ma".
(* ********************************************** *)