# HG changeset patch
# User kuncar
# Date 1393351634 -3600
# Node ID f1ed1e9cd080fb14e2fe8cdb607a7787a94fbb89
# Parent  81ba6249361056b267130ed31e0916df1f28bcb5
unregister lifting setup following the best practice of Lifting

diff -r 81ba62493610 -r f1ed1e9cd080 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Tue Feb 25 17:06:17 2014 +0000
+++ b/src/HOL/Code_Numeral.thy	Tue Feb 25 19:07:14 2014 +0100
@@ -928,6 +928,11 @@
 
 hide_const (open) Nat
 
+lifting_update integer.lifting
+lifting_forget integer.lifting
+
+lifting_update natural.lifting
+lifting_forget natural.lifting
 
 code_reflect Code_Numeral
   datatypes natural = _
diff -r 81ba62493610 -r f1ed1e9cd080 src/HOL/Library/Code_Target_Int.thy
--- a/src/HOL/Library/Code_Target_Int.thy	Tue Feb 25 17:06:17 2014 +0000
+++ b/src/HOL/Library/Code_Target_Int.thy	Tue Feb 25 19:07:14 2014 +0100
@@ -12,6 +12,10 @@
 
 declare [[code drop: integer_of_int]]
 
+context
+includes integer.lifting
+begin
+
 lemma [code]:
   "integer_of_int (int_of_integer k) = k"
   by transfer rule
@@ -86,6 +90,7 @@
 lemma [code]:
   "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
   by transfer rule
+end
 
 lemma (in ring_1) of_int_code_if:
   "of_int k = (if k = 0 then 0
@@ -105,7 +110,7 @@
 
 lemma [code]:
   "nat = nat_of_integer \<circ> of_int"
-  by transfer (simp add: fun_eq_iff)
+  including integer.lifting by transfer (simp add: fun_eq_iff)
 
 code_identifier
   code_module Code_Target_Int \<rightharpoonup>
diff -r 81ba62493610 -r f1ed1e9cd080 src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Tue Feb 25 17:06:17 2014 +0000
+++ b/src/HOL/Library/Code_Target_Nat.thy	Tue Feb 25 19:07:14 2014 +0100
@@ -10,6 +10,10 @@
 
 subsection {* Implementation for @{typ nat} *}
 
+context
+includes natural.lifting integer.lifting
+begin
+
 lift_definition Nat :: "integer \<Rightarrow> nat"
   is nat
   .
@@ -96,6 +100,8 @@
   "num_of_nat = num_of_integer \<circ> of_nat"
   by transfer (simp add: fun_eq_iff)
 
+end
+
 lemma (in semiring_1) of_nat_code_if:
   "of_nat n = (if n = 0 then 0
      else let
@@ -120,7 +126,7 @@
 
 lemma [code abstract]:
   "integer_of_nat (nat k) = max 0 (integer_of_int k)"
-  by transfer auto
+  including integer.lifting by transfer auto
 
 lemma term_of_nat_code [code]:
   -- {* Use @{term Code_Numeral.nat_of_integer} in term reconstruction
@@ -139,7 +145,7 @@
   "nat_of_integer 0 = 0"
   "nat_of_integer 1 = 1"
   "nat_of_integer (numeral k) = numeral k"
-  by (transfer, simp)+
+  including integer.lifting by (transfer, simp)+
 
 code_identifier
   code_module Code_Target_Nat \<rightharpoonup>