aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--etc/isa/multiple/C.thy5
-rw-r--r--etc/isa/multiple/foobar/foo.ML4
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;