Computer Supported Modeling and Reasoning
Exercises


Exercise Sheets

  1. Sheet (17.10.2001), IFOL.thy, FOL.thy
  2. Sheet (26.10.2001)
  3. Sheet (2.11.2001), NSet.thy
  4. Sheet (9.11.2001)
  5. Sheet (16.11.2001), RED.thy, CONV.thy, CNUM.thy
  6. Sheet (23.11.2001), LF.thy, Prop.thy
  7. Sheet (30.11.2001), HOL_POOR.thy
  8. (no special sheet for week 8) (7.12.2001)
  9. Sheet, HOL_BASIC.thy, HOL_BASIC.ML
  10. Sheet (14.12.2001)
  11. Sheet (11.1.2002)
  12. Sheet (18.1.2002)
  13. Sheet (25.1.2002), AVL_fragment.thy
  14. Sheet (1.2.2002), AVL_fragment2.thy
  15. Sheet (8.2.2002), AVL_fragment.ML

Configuring your system for Isabelle

Open a shell and type setup isabelle in it. In future sessions, this command should be invoked automatically. For this purpose, add the following line to your shell configuration file (called .cshrc if your shell is the c-shell or tc-shell): 
setup isabelle
You will always run Isabelle by starting emacs, and it is important that you start emacs from the shell (and not using, say, pop-up menus of your window manager). But before starting emacs, add the following lines to your .emacs file: 
(load-file "/usr/local/ProofGeneral-3.1/generic/proof-site.el")

(custom-set-variables
 '(proof-multiple-frames-enable t)
 '(proof-electric-terminator-enable t)
 '(proof-toolbar-use-button-enablers t)
 '(isabelle-prog-name "isabelle FOL")
 '(proof-x-symbol-enable t)
 '(query-user-mail-address nil)
 '(proof-toolbar-enable t))
(custom-set-faces)
For the first week's exercises, create a working directory and include the files IFOL.thy and FOL.thy. Now type xemacs ex1.ML and write 
use_thy "FOL";
in the file ex1.ML. This will invoke Isabelle in such a way that you are set up for the first week's exercises.
These pages will be updated as the lecture proceeds. You might also want to have a look at last year's page

Softech Home

Literature

Slides

Exercises

Jan-Georg Smaus
Last modified: Thu Oct 17 15:26:16 MEST 2002