src/HOL/Library/Numeral_Type.thy
changeset 29999 da85a244e328
parent 29998 19e1ef628b25
child 30001 dd27e16677b2
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Thu Feb 19 17:11:12 2009 -0800
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Thu Feb 19 17:13:35 2009 -0800
     1.3 @@ -347,11 +347,11 @@
     1.4  
     1.5  text {* Set up cases, induction, and arithmetic *}
     1.6  
     1.7 -lemmas bit0_cases [cases type: bit0, case_names of_int] = bit0.cases
     1.8 -lemmas bit1_cases [cases type: bit1, case_names of_int] = bit1.cases
     1.9 +lemmas bit0_cases [case_names of_int, cases type: bit0] = bit0.cases
    1.10 +lemmas bit1_cases [case_names of_int, cases type: bit1] = bit1.cases
    1.11  
    1.12 -lemmas bit0_induct [induct type: bit0, case_names of_int] = bit0.induct
    1.13 -lemmas bit1_induct [induct type: bit1, case_names of_int] = bit1.induct
    1.14 +lemmas bit0_induct [case_names of_int, induct type: bit0] = bit0.induct
    1.15 +lemmas bit1_induct [case_names of_int, induct type: bit1] = bit1.induct
    1.16  
    1.17  lemmas bit0_iszero_number_of [simp] = bit0.iszero_number_of
    1.18  lemmas bit1_iszero_number_of [simp] = bit1.iszero_number_of