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