diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 1999-10-27 15:20:49 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 1999-10-27 15:20:49 +0000 |
| commit | 3972a7eccf83aa609d2a222223c1a51ed3a0cd20 (patch) | |
| tree | 718fa1f7bfa4395b4e20308f0cf4be2921423bda | |
| parent | fed6e45d564a7e2793540e1906e37fe8a8b2ea87 (diff) | |
test stray ML file;
| -rw-r--r-- | etc/isa/multiple/C.thy | 5 | ||||
| -rw-r--r-- | etc/isa/multiple/foobar/foo.ML | 4 |
2 files changed, 8 insertions, 1 deletions
diff --git a/etc/isa/multiple/C.thy b/etc/isa/multiple/C.thy index 57816cd3..3316eaee 100644 --- a/etc/isa/multiple/C.thy +++ b/etc/isa/multiple/C.thy @@ -4,4 +4,7 @@ Logic Image: Pure *) -C = A + B +theory C = A + B +files "foobar/foo.ML": + +end diff --git a/etc/isa/multiple/foobar/foo.ML b/etc/isa/multiple/foobar/foo.ML new file mode 100644 index 00000000..25084a22 --- /dev/null +++ b/etc/isa/multiple/foobar/foo.ML @@ -0,0 +1,4 @@ + +val foo = "foo"; + +val bar = 1; |