next up previous contents
Next: Introduction Up: thesis Previous: Contents   Contents


List of Figures

  1. Pcoq's three-paned design
  2. Proof General
  3. Backwards proof
  4. Igloo's system design
  5. Mediator public member functions
  6. Building a PGIP message
  7. Igloo's main window
  8. Igloo's proof window
  9. Igloo's main window
  10. Initiating a connection to the Isabelle Server
  11. Successful connection to the Isabelle Server
  12. Begin a new theory
  13. Naming a new theory
  14. Naming theories to inherit
  15. Igloo's proof window
  16. Start a new theorem
  17. Naming the new theorem
  18. Defining a new theorem
  19. Initial proof state
  20. Initial subgoals
  21. Apply induction to a subgoal
  22. Second proof state
  23. Theorem split into base and inductive cases
  24. Simplify the base case
  25. Second proof state
  26. Removing an earlier proof state from the display
  27. Inductive subgoal remains
  28. Simplifying the inductive case
  29. Third proof state
  30. A complete proof


\begin{thesisabstract} In this thesis we present a prototypical user interface f... ...om powerful but complex theorem provers such as Isabelle. \end{thesisabstract}


\begin{thesisacknowledgments} I am indebted to a number of people for their help... ...ast, thanks go to Kate for being so understanding. \end{thesisacknowledgments}


2003-11-08

Valid HTML 3.2! Valid CSS!