src/HOL/Library/Code_Target_Int.thy
changeset 65552 f533820e7248
parent 64997 067a6cca39f0
child 68028 1f9f973eed2a
--- a/src/HOL/Library/Code_Target_Int.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/Library/Code_Target_Int.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Implementation of integer numbers by target-language integers\<close>
 
 theory Code_Target_Int
-imports "../GCD"
+imports Main
 begin
 
 code_datatype int_of_integer
@@ -22,11 +22,11 @@
 
 lemma [code]:
   "Int.Pos = int_of_integer \<circ> integer_of_num"
-  by transfer (simp add: fun_eq_iff) 
+  by transfer (simp add: fun_eq_iff)
 
 lemma [code]:
   "Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num"
-  by transfer (simp add: fun_eq_iff) 
+  by transfer (simp add: fun_eq_iff)
 
 lemma [code_abbrev]:
   "int_of_integer (numeral k) = Int.Pos k"
@@ -37,7 +37,7 @@
   by transfer simp
 
 context
-begin  
+begin
 
 qualified definition positive :: "num \<Rightarrow> int"
   where [simp]: "positive = numeral"