src/HOL/Codegenerator_Test/Generate_Target_MLton.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate_Target_MLton.thy	Tue Jan 28 13:02:42 2025 +0100
@@ -0,0 +1,14 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+section \<open>Test of target-language specific implementations for MLton\<close>
+
+theory Generate_Target_MLton
+  imports
+    "HOL-Codegenerator_Test.Generate_Target_String_Literals"
+    "HOL-Codegenerator_Test.Generate_Target_Bit_Operations"
+begin
+
+test_code Generate_Target_String_Literals.check in MLton
+test_code Generate_Target_Bit_Operations.check in MLton
+
+end
\ No newline at end of file