-
Notifications
You must be signed in to change notification settings - Fork 142
Proof
myreen edited this page Aug 8, 2012
·
11 revisions
This page lists an number of useful tactics together with a few examples that illustrate their use. We also comment on what makes a proof robust or fragile.
- rw, fs, lrw, simp, ...
- srw_ss, std_ss, bool_ss, pure_ss
- ARITH_ss
- DNF_ss
- link to writing custom simpsets etc.
- qmatch{_assum,}_abbrev_tac
- qabbrev_tac
- unabbrev_all_tac
- markerTheory.Abbrev_def
- qmatch{_assum,}_rename_tac
- qx_gen_tac
- X_CHOOSE_THEN
- qpat_abbrev_tac
- qpat_assum
- export rewrites
- NO_TAC, TRY, ORELSE, THEN1
- FORALL_PROD, EXISTS_PROD, LAMBDA_PROD
- UNCURRY
- PairCases_on
- conj_asm{1,2}_tac
- CONJ_ASSOC, ...
- AC
- any support in simplifier?
- stuff like RIGHT_FORALL_IMP_THM
- QuantHeuristics
- proofManagerLib.save
- CONV_TAC
-
-, >>, ...