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]: