changeset 81113 | 6fefd6c602fa |
parent 77061 | 5de3772609ea |
child 82452 | 8b575e1fef3b |
--- a/src/HOL/Library/Code_Target_Nat.thy Fri Oct 04 13:22:35 2024 +0200 +++ b/src/HOL/Library/Code_Target_Nat.thy Fri Oct 04 13:29:33 2024 +0200 @@ -11,7 +11,7 @@ subsection \<open>Implementation for \<^typ>\<open>nat\<close>\<close> context -includes natural.lifting integer.lifting +includes natural.lifting and integer.lifting begin lift_definition Nat :: "integer \<Rightarrow> nat"