Apply a patch to lem_relation before Holmake runs

Author: myreen

examples/l3-machine-code/arm8/asl-equiv/get-armv8.6-hol-snapshot

@@ -2,3 +2,5 @@
 git clone https://github.com/HOL-Theorem-Prover/armv8.6-asl-snapshot.git
 cd armv8.6-asl-snapshot
 git checkout 7b8e94ba2e2d91fe8cdfdb21b18f36c70f772cb1
+cd ..
+patch armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem/lem_relationScript.sml < lem_relation_patch

examples/l3-machine-code/arm8/asl-equiv/lem_relation_patch

@@ -0,0 +1,27 @@
+--- armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem/lem_relationScript.sml	2025-05-07 22:17:55.522283790 +0200
++++ armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem/lem_relation_newScript.sml	2025-05-07 22:26:39.696443565 +0200
+@@ -416,13 +416,13 @@
+ 
+ (*val reflexiveTransitiveClosureOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> rel 'a 'a*)
+ val _ = Define `
+- ((reflexive_transitive_closure_on:('a#'a)set -> 'a set ->('a#'a)set) r s=  (tc (((r) UNION ((relIdOn s))))))`;
++ ((reflexive_transitive_closure_on:('a#'a)set -> 'a set ->('a#'a)set) r s=  (transitive_closure (((r) UNION ((relIdOn s))))))`;
+ 
+ 
+ 
+ (*val reflexiveTransitiveClosure : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> rel 'a 'a*)
+ val _ = Define `
+- ((reflexiveTransitiveClosure:('a#'a)set ->('a#'a)set) r=  (tc (((r) UNION (relId)))))`;
++ ((reflexiveTransitiveClosure:('a#'a)set ->('a#'a)set) r=  (transitive_closure (((r) UNION (relId)))))`;
+ 
+ 
+ 
+@@ -438,7 +438,7 @@
+ (*val withoutTransitiveEdges: forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> rel 'a 'a*)
+ val _ = Define `
+  ((withoutTransitiveEdges:('a#'a)set ->('a#'a)set) r=
+-   (let tc1 = (tc r) in
++   (let tc1 = (transitive_closure r) in
+   {(a, c) | a, c 
+   | ((a, c) IN r) /\
+    (! (b :: range r).