doc-src/TutorialI/settings.ML
author wenzelm
Mon, 24 Sep 2007 13:52:51 +0200
changeset 24689 ac5b5a6155dd
parent 22097 7ee0529c5674
child 37216 3165bc303f66
permissions -rw-r--r--
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML; replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
22097
7ee0529c5674 renamed IsarOutput to ThyOutput;
wenzelm
parents: 9834
diff changeset
     1
(* $Id$ *)
7ee0529c5674 renamed IsarOutput to ThyOutput;
wenzelm
parents: 9834
diff changeset
     2
7ee0529c5674 renamed IsarOutput to ThyOutput;
wenzelm
parents: 9834
diff changeset
     3
ThyOutput.indent := 5;