doc-src/TutorialI/Documents/ROOT.ML
author blanchet
Tue, 17 Feb 2009 14:01:54 +0100
changeset 29956 62f931b257b7
parent 11647 0538cb0f7999
permissions -rw-r--r--
Reintroduce set_interpreter for Collect and op :. I removed them by accident when removing old code that dealt with the "set" type. Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11647
0538cb0f7999 initial setup for chapter on document preparation;
wenzelm
parents:
diff changeset
     1
0538cb0f7999 initial setup for chapter on document preparation;
wenzelm
parents:
diff changeset
     2
use_thy "Documents";