# HG changeset patch
# User hoelzl
# Date 1390484034 -3600
# Node ID ffabc0a5853ef73e7b0685e015b4e2cff1d829d2
# Parent  a389b50e6a42f87e41f7c75063077f76d08ce5e6
hide extended.Fin in code generator output

diff -r a389b50e6a42 -r ffabc0a5853e src/HOL/Library/Extended.thy
--- a/src/HOL/Library/Extended.thy	Thu Jan 23 14:26:16 2014 +0100
+++ b/src/HOL/Library/Extended.thy	Thu Jan 23 14:33:54 2014 +0100
@@ -77,12 +77,16 @@
 instance ..
 end
 
+declare zero_extended_def[symmetric, code_post]
+
 instantiation extended :: (one)one
 begin
 definition "1 = Fin(1::'a)"
 instance ..
 end
 
+declare one_extended_def[symmetric, code_post]
+
 instantiation extended :: (plus)plus
 begin
 
@@ -155,13 +159,13 @@
 
 instance extended :: ("{ab_semigroup_add,one}")numeral ..
 
-lemma Fin_numeral: "Fin(numeral w) = numeral w"
+lemma Fin_numeral[code_post]: "Fin(numeral w) = numeral w"
   apply (induct w rule: num_induct)
   apply (simp only: numeral_One one_extended_def)
   apply (simp only: numeral_inc one_extended_def plus_extended.simps(1)[symmetric])
   done
 
-lemma Fin_neg_numeral: "Fin (- numeral w) = - numeral w"
+lemma Fin_neg_numeral[code_post]: "Fin (- numeral w) = - numeral w"
 by (simp only: Fin_numeral uminus_extended.simps[symmetric])