doc-src/IsarTut/Tutorial/ROOT.ML
author gagern
Fri, 01 Apr 2005 18:40:14 +0200
changeset 15646 b45393fb38c0
parent 13202 53022e5f73ff
permissions -rw-r--r--
bring make to delete files on error


set quick_and_dirty;

use_thy "Tutorial";