Tactics

• Introduction
  • Conventions
  • Universes and Level Expressions
  • Formula Structure
  • Soft Abstractions
  • The Sequent
  • Proof Annotations
    • Goal Labels
    • Tactic Arguments
  • Matching and Substitution
• Basic
  • Structural
  • Single-Step Decomposition
  • Iterated Decomposition
• Tacticals
  • Basic Tacticals
  • Label Sensitive Tacticals
  • Multiple Clause Tacticals
• Case Splits and Induction
• Forward and Backward Chaining
• Decision Procedures
  • ProveProp
  • Eq
  • RelRST
  • Arith
  • SupInf
    • Description
    • Details
• Rewriting
  • Introduction
  • Concise Rewriting Tactics
  • Introduction to Conversions
  • Nuprl Conversions
  • Conversion Descriptions
    • Trivial Conversions
    • Lemma and Hypothesis Conversions
    • Atomic Direct-Computation Conversions
    • Attributed Abstractions
    • Abstract Redices
    • Reduction Strengths and Forces
    • Composite Direct Computation Conversions
    • Macro Conversions
    • Conversionals
  • Applying Conversions
  • Lemma Support
    • Functionality Lemmas
    • Transitivity Lemmas
    • Weakening Lemmas
    • Inversion Lemmas
  • Environments
  • Relations
    • Introduction
    • Declaring Relations
  • Justifications
  • Substitution
• Type Inclusion
• Miscellaneous
• Autotactics
• Transformation Tactics
• Constructive and Classical Reasoning
  • Constructive Reasoning
  • Decidability
  • Squash Stability and Hidden Hypotheses
  • Classical Reasoning
• Further Information