FTBFS HolBdd and temporal_deep examples

HOL-Theorem-Prover · Jan 17, 2024 · 4103c90 · 4103c90
1 parent 7a632cd
commit 4103c90
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/examples/HolBdd/MachineTransitionScript.sml b/examples/HolBdd/MachineTransitionScript.sml
@@ -990,13 +990,15 @@ val TotalMooreTrans =
     THEN Q.EXISTS_TAC `(q',nextfn(q,r))`
     THEN RW_TAC std_ss [MooreTrans_def]);
 
+(* NOTE: duplicated with the next theorem but let's keep the original code:
 val ReachableMooreTrans =
  save_thm
   ("ReachableMooreTrans",
    SPECL
     [``\(input:'a,state:'b). (input = inputs 0) /\ (state = states 0)``,
      ``(input:'a, state:'b)``]
     (MATCH_MP ReachablePath TotalMooreTrans));
+ *)
 
 (*****************************************************************************)
 (*   val ReachableMooreTrans =                                               *)

diff --git a/examples/temporal_deep/src/model_check/selftest.sml b/examples/temporal_deep/src/model_check/selftest.sml
@@ -25,7 +25,7 @@ fun modelCheck_test1 () = let
 in
   if aconv (concl (valOf test1)) result1 then OK ()
   else die ("Got " ^ term_to_string (concl (valOf test1)));
-  Process.system ("rm " ^ (!model_check_temp_file)))
+  Process.system ("rm " ^ (!model_check_temp_file))
 end;
 
 fun modelCheck_test2 () = let
@@ -34,7 +34,7 @@ in
   if (isSome test2) then
     die ("Got " ^ term_to_string (concl (valOf test2)))
   else OK ();
-  Process.system ("rm " ^ (!model_check_temp_file)))
+  Process.system ("rm " ^ (!model_check_temp_file))
 end;
 
 val _ = modelCheck_test1 ();