src/HOL/Quickcheck_Narrowing.thy
changeset 46032 0da934e135b0
parent 45818 53a697f5454a
child 46308 e5abbec2697a
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Thu Dec 29 10:47:56 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Dec 29 10:47:56 2011 +0100
     1.3 @@ -134,15 +134,10 @@
     1.4  lemma zero_code_int_code [code, code_unfold]:
     1.5    "(0\<Colon>code_int) = Numeral0"
     1.6    by (simp add: number_of_code_int_def Pls_def)
     1.7 -lemma [code_post]: "Numeral0 = (0\<Colon>code_int)"
     1.8 -  using zero_code_int_code ..
     1.9  
    1.10  lemma one_code_int_code [code, code_unfold]:
    1.11    "(1\<Colon>code_int) = Numeral1"
    1.12    by (simp add: number_of_code_int_def Pls_def Bit1_def)
    1.13 -lemma [code_post]: "Numeral1 = (1\<Colon>code_int)"
    1.14 -  using one_code_int_code ..
    1.15 -
    1.16  
    1.17  definition div_mod_code_int :: "code_int \<Rightarrow> code_int \<Rightarrow> code_int \<times> code_int" where
    1.18    [code del]: "div_mod_code_int n m = (n div m, n mod m)"