1structure preamble = 2struct 3open HolKernel Parse boolLib bossLib; 4open ASCIInumbersTheory BasicProvers Defn HolKernel Parse SatisfySimps Tactic 5 monadsyntax alistTheory alignmentTheory arithmeticTheory boolLib 6 boolSimps bossLib containerTheory combinTheory dep_rewrite 7 finite_mapTheory indexedListsTheory listTheory llistTheory 8 markerLib mp_then optionTheory pairLib 9 pairTheory pred_setTheory quantHeuristicsLib relationTheory 10 rich_listTheory sortingTheory stringTheory sumTheory; 11val wf_rel_tac = WF_REL_TAC; 12val every_case_tac = BasicProvers.EVERY_CASE_TAC; 13val full_case_tac = BasicProvers.FULL_CASE_TAC; 14val sym_sub_tac = SUBST_ALL_TAC o SYM; 15fun asm_match q = Q.MATCH_ASSUM_RENAME_TAC q; 16val match_exists_tac = part_match_exists_tac (hd o strip_conj); 17val asm_exists_tac = first_assum(match_exists_tac o concl); 18val rveq = rpt var_eq_tac; 19end 20