Tactic Usage (with number of proof nodes citing each tactic name) sorted alphabetically, throughout /home/nuprl/nuprl4/lib/theories/standard/num_thy_1.thy /home/nuprl/nuprl4/lib/theories/standard/list_1.thy /home/nuprl/lib/theories/standard/int_2.thy /home/nuprl/nuprl4/lib/theories/standard/union.thy /home/nuprl/nuprl4/lib/theories/standard/rel_1.thy /home/nuprl/nuprl4/lib/theories/standard/fun_1.thy /home/nuprl/nuprl4/lib/theories/standard/quot_1.thy /home/nuprl/nuprl4/lib/theories/standard/prog_1.thy /home/nuprl/nuprl4/lib/theories/standard/rfunction_1.thy /home/nuprl/nuprl4/lib/theories/standard/bool_1.thy /home/nuprl/nuprl4/lib/theories/standard/core_2.thy /home/nuprl/nuprl4/lib/theories/standard/sqequal_1.thy /home/nuprl/nuprl4/lib/theories/standard/int_1.thy /home/nuprl/nuprl4/lib/theories/standard/isect_1.thy /home/nuprl/nuprl4/lib/theories/standard/ml_1.thy /home/nuprl/nuprl4/lib/theories/standard/well_fnd.thy /home/nuprl/nuprl4/lib/theories/standard/rules_1.thy /home/nuprl/nuprl4/lib/theories/standard/core_1.thy /home/nuprl/nuprl4/lib/theories/standard/boot.thy 2 AGenRepD (string list)->tactic 2 ARepD (string list)->tactic 1 AbEval (tok list)->int->tactic 63 AbReduce int->tactic 2 AbSetEqTypeCD tactic 1 AbSetHD int->tactic 7 AddHiddenLabel tok->tactic 1 AllBoolInd tactic 5 ApFunToHypEquands var->term->term->int->tactic 1 ApplyFunToHypEquands term->int->tactic 18 Arith tactic 1 ArithMemberReflEqTypeCD tactic 65 ArithSimp int->tactic 80 Assert term->tactic 1 AssertAtHyp int->term->tactic 4 AssertL (term list)->tactic 12 AssertLemma tok->(term list)->tactic 5 At term->tactic->tactic 1814 Auto tactic 45 Auto' tactic 32 BHyp int->tactic 77 BLemma tok->tactic 1 BackThruGenLemma tok->int->tactic 49 BackThruHyp int->tactic 81 BackThruLemma tok->tactic 3 BackThruLemmaWithUnfolds tok->(tok list)->tactic 12 Backchain (tok list)->tactic 1 BasicSetHD int->tactic 7 BasicSquashHD int->tactic 4 BoolCases int->tactic 16 BoolCasesOnCExp term->tactic 12 BoolEval tactic 13 BoolInd int->tactic 8 CDToVarThen var->(int->tactic)->tactic 1 CSquash tactic 1 CUnhide tactic 2 CaseReduce tok->(int list)->tactic 1 Cases (term list)->tactic 15 CompNatInd int->tactic 3 Complete tactic->tactic 1 CondRewriteWith tactic->(int list)->(tok list)->int->tactic 1 Contradiction tactic 2 CopyToEnd int->tactic 374 D int->tactic 28 DNth int->int->tactic 21 DTerm term->int->tactic 2 DVars (var list)->int->tactic 62 Decide term->tactic 1 Declaration tactic 1 EnumCasesTac tactic 1 EnumEqFalseTac tactic 1 EnumEqTrueTac tactic 1 EnumSqTypeTac tactic 1 Eq tactic 8 EqCD tactic 2 EqHD int->tactic 3 EqIntCases int->tactic 2 EqTypeCD tactic 3 EqTypeD int->tactic 1 EqTypeHD int->tactic 6 ExRepD tactic 8 ExistHD int->tactic 2 Ext tactic 7 ExtWith (var list)->(term list)->tactic 20 FHyp int->(int list)->tactic 37 FLemma tok->(int list)->tactic 6 Fail tactic 2 Fiat tactic 10 Fold tok->int->tactic 6 FunElim term->tactic 1 FwdThruGenLemma tok->int->(int list)->tactic 4 FwdThruHyp int->(int list)->tactic 74 FwdThruLemma tok->(int list)->tactic 10 GenExRepD tactic 27 GenRepD tactic 48 GenUnivCD tactic 37 HypBackchain tactic 44 HypSubst int->int->tactic 7 Hypothesis tactic 11 Id tactic 4 IfLab tok->tactic->tactic->tactic 6 IfLabL (tok#tactic list)->tactic 2 Inclusion int->tactic 17 InstConcl (term list)->tactic 32 InstHyp (term list)->int->tactic 42 InstLemma tok->(term list)->tactic 6 IntInd int->tactic 1 InvImageInd term->term->(int->tactic)->int->tactic 1 InvertIff int->tactic 5 InvertRel int->tactic 9 Lemma tok->tactic 24 ListInd int->tactic 2 ListIndA int->tactic 36 MemCD tactic 14 MemEqCD tactic 5 MemTypeCD tactic 1 MemTypeHD int->tactic 9 MemberEqCD tactic 12 MoveToConcl int->tactic 1 NCompInd int->tactic 3 NInd int->tactic 1 NSubsetInd int->tactic 5 NatInd int->tactic 1 NegateConcl2 tactic 7 New (var list)->tactic->tactic 1 NotThinning tactic->tactic 4 NthDecl int->tactic 4 NthHyp int->tactic 1 ORELSE tactic->tactic->tactic 1 OnAllClauses (int->tactic)->tactic 3 OnAllHyps (int->tactic)->tactic 5 OnClauses (int list)->(int->tactic)->tactic 3 OnCls (int list)->(int->tactic)->tactic 43 OnHyps (int list)->(int->tactic)->tactic 5 OnMClauses (int list)->(int->tactic)->tactic 9 OnMCls (int list)->(int->tactic)->tactic 7 OnMHyps (int list)->(int->tactic)->tactic 14 OnVar var->(int->tactic)->tactic 4 PrimEqCD tactic 1 ProveDecidable tactic 36 ProveOpCombTyping tok->tactic 11 ProveProp tactic 9 ProveProp1 tactic 8 ProvePropertiesLemma tactic 2 ProveSqStable tactic 4 PushArgs (tok#[arg%4723%909] list)->tactic 7 RA tactic->tactic 34 RW convn->int->tactic 1 RWAddr (int list)->convn->int->tactic 121 RWH convn->int->tactic 28 RWN int->convn->int->tactic 4 RWNth int->convn->int->tactic 17 RWO string->int->tactic 7 RWW string->int->tactic 3 RankInd term->term->(int->tactic)->int->tactic 17 RecCaseSplit tok->tactic 1 RecCaseSplitNth int->tok->tactic 2 RecEval (tok list)->int->tactic 1 RecFold tok->int->tactic 9 RecUnfold tok->int->tactic 38 Reduce int->tactic 1 Refine tok->(argument list)->tactic 16 RelRST tactic 5 RenameVar var->int->tactic 75 RepD tactic 14 RepUnfolds (tok list)->int->tactic 9 Repeat tactic->tactic 6 RepeatFor int->tactic->tactic 8 RepeatMFor int->tactic->tactic 1 RepeatOrHD int->tactic 1 ReplaceWith term->int->tactic 4 ReplaceWithEqv convn->term->int->tactic 16 RevHypSubst int->int->tactic 29 Rewrite convn->int->tactic 8 RewriteWith (int list)->(tok list)->int->tactic 113 SIAuto tactic 38 Sel int->tactic->tactic 7 SeqOnM (tactic list)->tactic 1 SetEqTypeCD tactic 3 Simple tactic->tactic 7 SoftNthHyp int->tactic 6 SplitITE int->tactic 31 SplitOnConclITE tactic 6 SplitOnConclITEs tactic 2 SqEqual tactic 6 SqSubstAtAddr (int list)->term->int->tactic 4 SquashCD tactic 1 SquashEqTypeCD tactic 1 StrengthenRel tactic 3 StrongAuto tactic 1 Subst term->int->tactic 1 SubstClause term->int->tactic 2 SupInf tactic 1 SupInf' tactic 4 SwapEquands int->tactic 1108 THEN tactic->tactic->tactic 66 Thin int->tactic 83 Trivial tactic 2 TrivializeConcl tactic 20 Try tactic->tactic 4 TryOnAllClauses (int->tactic)->tactic 1 TryOnAllHyps (int->tactic)->tactic 313 Unfold tok->int->tactic 1 UnfoldAtAddr (int list)->int->tactic 1 UnfoldTop tok->int->tactic 12 UnfoldTopAb int->tactic 54 Unfolds (tok list)->int->tactic 1 Unhide tactic 1 UnhideSinceCompTrivialConcl tactic 4 UnhideSinceSquashedConcl tactic 2 UnhideSqStableHyp int->tactic 1 UnitInd int->tactic 240 UnivCD tactic 8 UnivFmlaCD (var list)->tactic 2 UseEqWitness term->tactic 3 UseWitness term->tactic 50 Using (var#term list)->tactic->tactic 2 WFndHypInd int->int->tactic 81 With term->tactic->tactic 2 YRecModulePiTac int->tok->(tok list)->tactic 1 get_tactic_arg tok->proof->tactic