src/HOL/Int.thy
changeset 31100 6a2e67fe4488
parent 31068 f591144b0f17
child 31998 2c7a24f74db9
equal deleted inserted replaced
31092:27a6558e64b6 31100:6a2e67fe4488
  1519   of_int_0 of_int_1 of_int_add of_int_mult
  1519   of_int_0 of_int_1 of_int_add of_int_mult
  1520 
  1520 
  1521 use "Tools/numeral_simprocs.ML"
  1521 use "Tools/numeral_simprocs.ML"
  1522 
  1522 
  1523 use "Tools/int_arith.ML"
  1523 use "Tools/int_arith.ML"
       
  1524 setup {* Int_Arith.global_setup *}
  1524 declaration {* K Int_Arith.setup *}
  1525 declaration {* K Int_Arith.setup *}
  1525 
  1526 
  1526 setup {*
  1527 setup {*
  1527   ReorientProc.add
  1528   ReorientProc.add
  1528     (fn Const (@{const_name number_of}, _) $ _ => true | _ => false)
  1529     (fn Const (@{const_name number_of}, _) $ _ => true | _ => false)