src/HOL/Library/Code_Target_Nat.thy
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"