src/HOL/Integ/IntDef.thy
changeset 18708 4b3dadb4fe33
parent 18704 2c86ced392a8
child 18757 f0d901bc0686
     1.1 --- a/src/HOL/Integ/IntDef.thy	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Integ/IntDef.thy	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -948,12 +948,12 @@
     1.4  
     1.5  *}
     1.6  
     1.7 -setup {*[
     1.8 -  Codegen.add_codegen "number_of_codegen" number_of_codegen,
     1.9 +setup {*
    1.10 +  Codegen.add_codegen "number_of_codegen" number_of_codegen #>
    1.11    CodegenPackage.add_appconst
    1.12 -    ("Numeral.number_of", ((1, 1), CodegenPackage.appgen_number_of mk_int_to_nat bin_to_int "IntDef.int" "nat")),
    1.13 +    ("Numeral.number_of", ((1, 1), CodegenPackage.appgen_number_of mk_int_to_nat bin_to_int "IntDef.int" "nat")) #>
    1.14    CodegenPackage.set_int_tyco "IntDef.int"
    1.15 -]*}
    1.16 +*}
    1.17  
    1.18  quickcheck_params [default_type = int]
    1.19