Go to the first, previous, next, last section, table of contents.

Index

Jump to: a - c - d - e - f - g - i - l - m - n - o - p - r - s - t - u - x

a

  • Arbitrary rule
  • Associated files
  • Author's address

    • c

  • Choosing which logic
  • Classical rule set
  • comint
  • comint-dynamic-complete
  • Compatible Emacs versions
  • Creating rule tables
  • Customizing the display

    • d

  • Definition
  • Designated subgoal
  • Destruction rule
  • Display customization
  • Dreams

    • e

  • Editing ML files
  • Editing theory files
  • Elimination rule

    • f

  • font-lock-keywords
  • Fontification
  • Frame customization
  • ftp
  • Future plans

    • g

  • `goalify.el' file

    • i

  • Indexed tactic
  • Installing Isamode
  • Interacting with Isabelle
  • Interaction buffer
  • Interaction menu operations
  • Introduction rule
  • isa-add-theory-rulegroup
  • isa-add-theory-rules
  • isa-asm_full_simp_tac
  • isa-asm_simp_tac
  • isa-assume_tac
  • isa-auto-backslashes
  • isa-back
  • isa-batchify
  • isa-best_tac
  • isa-chop
  • isa-choplev
  • isa-completion-list
  • isa-contr_tac
  • isa-cut_facts_tac
  • isa-cut_facts_tac-prems
  • isa-default-menubar
  • isa-dmatch_tac
  • isa-dresolve_tac
  • isa-ematch_tac
  • isa-eq_assume_tac
  • isa-eq_mp_tac
  • isa-eresolve_tac
  • isa-expandshorts
  • isa-fast_tac
  • isa-fold_goals_tac
  • isa-forward_tac
  • isa-goal-thy
  • isa-goalw-thy
  • isa-match_tac
  • isa-match_tac-prems
  • isa-menus
  • isa-ml-file-extension
  • isa-mp_tac
  • isa-multi-frame-display-props
  • isa-multiple-frame-mode
  • isa-pop-proof
  • isa-possible-associated-buffer-names
  • isa-push-proof
  • isa-resolve_tac
  • isa-resolve_tac-prems
  • isa-result
  • isa-rewrite_goals_tac
  • isa-rewrite_tac
  • isa-rotate-proofs
  • isa-ruletable-paths
  • isa-session-prelude
  • isa-simp_tac
  • isa-single-frame-display-props
  • isa-startup-defaults
  • isa-step_tac
  • isa-theory-rules
  • isa-thy-find-other-file
  • isa-thy-heading-indent
  • isa-thy-indent-level
  • isa-thy-indent-strings
  • isa-thy-insert-template
  • isa-thy-mode
  • isa-thy-mode-font-lock-keywords
  • isa-thy-use-buffer
  • isa-thy-use-line
  • isa-thy-use-region
  • isa-thy-use-sml-mode
  • isa-toggle-multi-frame
  • isa-unbatchify
  • isa-undo
  • isabelle
  • isabelle-session
  • Isamode

    • l

  • Large proof states
  • listener
  • Listener buffer
  • Listener commands
  • listener-minor-mode
  • Logic
  • Logic Image comment

    • m

  • ML
  • ML identifiers
  • ML mode (sml-mode)
  • ML types

    • n

  • Naming conventions

    • o

  • Obtaining Isamode

    • p

  • Proof levels
  • Proof state buffer
  • proofstate

    • r

  • Rule categories
  • Rule set
  • Rule tables
  • Rule tables, format
  • Rule tables, making
  • Rule, arbitrary
  • Rule, destruction
  • Rule, elimination
  • Rule, introduction
  • ruletable
  • Ruletable commands

    • s

  • Simplifier rule set
  • sml-mode
  • Subgoal list

    • t

  • Tactic
  • Tactic, indexed
  • Theory files
  • Theory files, highlighting
  • Theory mode user options

    • u

  • User options, display
  • User options, logic image path
  • User options, theory mode

    • x

  • X Resources

    • Go to the first, previous, next, last section, table of contents.