# HG changeset patch
# User haftmann
# Date 1325152076 -3600
# Node ID 0da934e135b089b4688e3f0c4017afd631c035f3
# Parent  ac6bae9fdc2f0a2c11b03ed576284b773f08305a
dropped redundant setup

diff -r ac6bae9fdc2f -r 0da934e135b0 src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Dec 29 10:47:56 2011 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Dec 29 10:47:56 2011 +0100
@@ -134,15 +134,10 @@
 lemma zero_code_int_code [code, code_unfold]:
   "(0\<Colon>code_int) = Numeral0"
   by (simp add: number_of_code_int_def Pls_def)
-lemma [code_post]: "Numeral0 = (0\<Colon>code_int)"
-  using zero_code_int_code ..
 
 lemma one_code_int_code [code, code_unfold]:
   "(1\<Colon>code_int) = Numeral1"
   by (simp add: number_of_code_int_def Pls_def Bit1_def)
-lemma [code_post]: "Numeral1 = (1\<Colon>code_int)"
-  using one_code_int_code ..
-
 
 definition div_mod_code_int :: "code_int \<Rightarrow> code_int \<Rightarrow> code_int \<times> code_int" where
   [code del]: "div_mod_code_int n m = (n div m, n mod m)"