Fix quote-filter test for Moscow ML

HOL-Theorem-Prover · Dec 18, 2024 · a199c1a · a199c1a
1 parent 5bbb8a2
commit a199c1a
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/tools/Holmake/tests/quote-filter/expected-mosml b/tools/Holmake/tests/quote-filter/expected-mosml
@@ -93,3 +93,12 @@ val x = 92 + 10;
 val   y = 11
 val s = ""  
 val s' = "foo.sml" (* #(FILE) *)
+
+val thm = Q.store_thm_at (DB_dtype.mkloc ("foo.sml", 15, true)) ("thm[foo, simp , key = val1 val2]", [QUOTE " (*#loc 15 42*)\n\
+\  p /\\ q"], (fn HOL__GOAL__foo => (
+
+  cheat
+) HOL__GOAL__foo));
+
+val thm2 = boolLib.save_thm("thm2[foo, simp , key = val1 val2]", exp
+);