Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/UNITY/Comp/Alloc.thy
changeset 82630 2bb4a8d0111d
parent 69813 9d94a6c95113 
--- a/src/HOL/UNITY/Comp/Alloc.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Sun May 18 14:33:01 2025 +0000
@@ -306,9 +306,9 @@
 (*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
 fun list_of_Int th =
     (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
-    handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
+    handle THM _ => (list_of_Int (th RS @{thm IntD1}) @ list_of_Int (th RS @{thm IntD2}))
     handle THM _ => (list_of_Int (th RS @{thm INT_D}))
-    handle THM _ => (list_of_Int (th RS bspec))
+    handle THM _ => (list_of_Int (th RS @{thm bspec}))
     handle THM _ => [th];
 \<close>
 
@@ -319,7 +319,7 @@
   fun normalized th =
     normalized (th RS spec
       handle THM _ => th RS @{thm lessThanBspec}
-      handle THM _ => th RS bspec
+      handle THM _ => th RS @{thm bspec}
       handle THM _ => th RS (@{thm guarantees_INT_right_iff} RS iffD1))
     handle THM _ => th;
 in
isabelle