Isamode

Theorem proving with Isabelle inside GNU Emacs

Isamode version 2.7, for Isabelle99.

May 2000.

• 1. Using Isabelle with Emacs
  • Features of Isamode
  • Prerequisites
• 2. Interacting with Isabelle
  • 2.1 Choosing which Logic
  • 2.2 Startup Sequence
  • 2.3 Completion
  • 2.4 Backslashes
  • 2.5 Menus
  • 2.6 Interaction mode menu operations
• 3. Proof state
  • 3.1 Proofstate Commands
  • 3.2 A note about large proof states
• 4. Rule tables
  • 4.1 Ruletable Commands
  • 4.2 Creating Rule tables
  • 4.3 Rule Categories
    • Naming convention table
    • Naming convention example
  • 4.4 Rule table internals
    • Rule table format
    • Rule table extension functions
• 5. Listening (and talking)
  • 5.1 Listener Commands
• 6. Theory and ML files
  • 6.1 Editing theory files
  • 6.2 Editing ML files
  • 6.3 Interactive and Batch Proofs
  • 6.4 Theory mode User Options
  • 6.5 Fontification of Theory Files
• 7. Customizing the Display
  • 7.1 Display options
  • 7.2 Display options, continued
  • 7.3 X Resources
• 8. Acknowledgements
• A. Obtaining the software
• B. Installing Isamode
• C. Ideas and Dreams
  • Proof stepping
  • Customization per-logic
  • Better theory handling
  • Improved Listener
  • Caching proof states
  • Rule table categories
  • Improved batchify
  • Tracing Output
  • Text insertion
  • Improved templates
  • Sensitizing rules
  • Buttons
  • Driving by mouse
  • Help from Isabelle
  • Bells and whistles
  • Special characters
  • Questions
• Index
• Copying

This document was generated on 18 May 2000 using texi2html 1.56k.