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