src/HOL/Divides.thy
changeset 66810 cc2b490f9dc4
parent 66808 1907167b6038
child 66814 a24cde9588bb
     1.1 --- a/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -527,25 +527,6 @@
     1.4  
     1.5  end
     1.6  
     1.7 -ML \<open>
     1.8 -structure Cancel_Div_Mod_Int = Cancel_Div_Mod
     1.9 -(
    1.10 -  val div_name = @{const_name divide};
    1.11 -  val mod_name = @{const_name modulo};
    1.12 -  val mk_binop = HOLogic.mk_binop;
    1.13 -  val mk_sum = Arith_Data.mk_sum HOLogic.intT;
    1.14 -  val dest_sum = Arith_Data.dest_sum;
    1.15 -
    1.16 -  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
    1.17 -
    1.18 -  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
    1.19 -    @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
    1.20 -)
    1.21 -\<close>
    1.22 -
    1.23 -simproc_setup cancel_div_mod_int ("(k::int) + l") =
    1.24 -  \<open>K Cancel_Div_Mod_Int.proc\<close>
    1.25 -
    1.26  lemma is_unit_int:
    1.27    "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
    1.28    by auto