Tools

• Automatic Proof Search (Auto)
  • Usage
  • Limitations
  • User feedback
• Command-line options
  • Command-line options
  • Command-line and pragma options
  • Consistency checking of options used
• Compilers
  • Backends
  • Optimizations
• Emacs Mode
  • quick-guide-introduction
  • Configuration
  • Keybindings
  • Unicode input
  • Highlight
• Literate Programming
  • Literate TeX
  • Literate reStructuredText
  • Literate Markdown
  • Literate Org
• Generating HTML
  • Options
• Generating LaTeX
  • Known pitfalls and issues
  • Options
  • Quicker generation without typechecking
  • Features
  • Examples
• Interface files
  • Storage
  • Compilation
• Library Management
  • Example: Using the standard library
  • Library files
  • Installing libraries
  • Using a library
  • Default libraries
  • Version numbers
  • Upgrading
• Performance debugging
  • Measuring typechecking performance
  • Measuring run-time performance
• Search Definitions in Scope
  • Usage