src/HOL/String.thy
changeset 81113 6fefd6c602fa
parent 80932 261cd8722677
child 81118 9e2eb05cc2b7
--- a/src/HOL/String.thy	Fri Oct 04 13:22:35 2024 +0200
+++ b/src/HOL/String.thy	Fri Oct 04 13:29:33 2024 +0200
@@ -180,7 +180,7 @@
   by (auto simp add: UNIV_char_of_nat card_image)
 
 context
-  includes lifting_syntax integer.lifting natural.lifting
+  includes lifting_syntax and integer.lifting and natural.lifting
 begin
 
 lemma [transfer_rule]: