diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-10-29 18:47:39 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-10-29 18:47:39 +0000 |
| commit | d607ce5cfd26922bea0ef61666805e4817cf3516 (patch) | |
| tree | 5b2b0a8321d8ee95f390e72d9ae7df6048dadc1d /etc/isa | |
| parent | 7d384343c6ea36d236e703945967b9ab72517fd4 (diff) | |
More notes
Diffstat (limited to 'etc/isa')
| -rw-r--r-- | etc/isa/multiple/README | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/etc/isa/multiple/README b/etc/isa/multiple/README index 4cd5aa71..0ea75fcc 100644 --- a/etc/isa/multiple/README +++ b/etc/isa/multiple/README @@ -42,11 +42,16 @@ Because of theory loader's odd behaviour, must watch what happens to ML files of autoloaded children. -1) visit example.ML, example.thy EFFECT: ML +1) visit example.ML, example.thy EFFECT: ML thy 2) assert .ML EFFECT: ML* thy* 3) retract thy EFFECT: ML thy (29.10.98 BREAKS!) get ML* +1) visit example.ML, example.thy ML thy +2) assert thy ML thy* (29.10.98: works, but + example.ML is on included + files list: Isabelle problem) + |