anchor.diff:  	    "  apply(simp add: zgcd_greatest_iff)"
   	    "  apply(rule dvd_antisym, auto, rule zgcd_geq_zero, simp add: zgcd_greatest_iff)"
   	    "  end-proof"
  -	    " "
  +	    (:optional "")
   	    " proof Isa -verbatim"
   	    "theorem Integer__gcd_is_zgcd[simp]: "
   	    "  \"Integer__gcd = zgcd\""
  
positive.code: 	    "        && gcd(x, y) divides x "
  	    "           && gcd(x, y) divides y "
  	    "              && (fa(w : Int) (w divides x && w divides y => gcd(x, y) >= w))"
  	    " "
  	    " proof Isa"
  	    "    apply(subgoal_tac \"0 < zgcd (x, y)\", auto)"
  	    "    apply(rule zdvd_imp_le, auto simp add: zgcd_greatest_iff)+"
  	    "    apply(rule classical, auto simp add: zgcd_def gcd_zero)+"
  	    "  end-proof"
  	    " "
  	    " theorem Integer.gcd_of_zero_zero_is_zero is gcd(0, 0) = 0"
  	    " "
  	    " theorem Integer.lcm_smallest_abs_multiple is "
  	    "    fa(x : Int, y : Int, w : Int0) "
  	    "     w multipleOf x && w multipleOf y => lcm(x, y) <= abs w"
  	    " "
  	    " proof Isa"
  	    "    apply(simp, drule_tac w=\"w\" and x=\"x\" and y=\"y\" in zlcm_least, simp_all)"
  	    "   apply(rule zdvd_imp_le, auto simp add: zdvd_abs2)"
  	    "  end-proof"
  	    " "
  	    " conjecture Integer./_Obligation_the is "
  	    "    fa(j : Int0, i : Int) j divides i => (ex1(k : Int) i = j * k)"
  	    " "
  	    " conjecture Integer./_Obligation_exhaustive is "
  	    "    fa(D : {(i, j) : (Int * Int0) | j divides i}) D.2 divides D.1"
  	    " "
  	    " op  / (((i, j) | j divides i) : {(i, j) : (Int * Int0) | j divides i})"
  	    "  infixl 26 : Int = the (k : Int) i = j * k"
  	    " "
  	    " conjecture Integer.divT_Obligation_the is "
  	    "    fa(j : Int0, i : Int) "
  	    "     ~(abs i < abs j) "
  	    "     => (ex1(q : Int) "
  	    "          sign q = sign i * sign j "
  	    "          && abs i - abs j < abs(q * j) && abs(q * j) <= abs i)"
  	    " "
  	    " op  divT ((i, j) : Int * Int0) infixl 26 : Int = "
  	    "   if abs i < abs j"
  	    "    then 0 "
  
negative.code: 	    "             && 14 modF -(5) = -(1) "
  	    "                && 11 modF -(5) = -(4) "
  	    "                   && -(14) modF -(5) = -(4) && -(11) modF -(5) = -(1)"
  	    (:optional "")
  	    " theorem Integer.exact_divF is "
  	    "    fa(i : Int, j : Int0) j divides i => i divF j = i / j"
  	    (:optional "")
  	    " theorem Integer.divF_is_largest is "
  	    "    fa(i : Int, j : Int0, k : Int) k * j <= i => k <= i divF j"
  	    (:optional "")
  	    " conjecture Integer.divF_of_negated_divisor_Obligation_subtype is "
  	    "    fa(j : Int0) - j ~= 0"
  	    (:optional "")
  	    " theorem Integer.divF_of_negated_divisor is "
  	    "    fa(i : Int, j : Int0) "
  	    "     i divF - j = -(i divF j) - (if j divides i then 0 else 1)"
  	    (:optional "")
  	    " theorem Integer.divF_of_negated_dividend is "
  	    "    fa(i : Int, j : Int0) "
  	    "     - i divF j = -(i divF j) - (if j divides i then 0 else 1)"
  	    (:optional "")
  	    " theorem Integer.divides_iff_modF_0 is "
  	    "    fa(i : Int, j : Int0) j divides i <=> i modF j = 0"
  	    (:optional "")
  	    " theorem Integer.modF_less_than_divisor_in_abs is "
  	    "    fa(i : Int, j : Int0) abs(i modF j) < abs j"
  	    (:optional "")
  	    " conjecture Integer.modF_of_negated_divisor_Obligation_subtype is "
  	    "    fa(j : Int0) - j ~= 0"
  	    (:optional "")
  	    " theorem Integer.modF_of_negated_divisor is "
  	    "    fa(i : Int, j : Int0) "
  	    "     i modF - j = i modF j - j * (if j divides i then 0 else 1)"
  	    (:optional "")
  	    " theorem Integer.modF_of_negated_dividend is "
  	    "    fa(i : Int, j : Int0) "
  	    "     - i modF j = -(i modF j) + j * (if j divides i then 0 else 1)"
  	    (:optional "")
  	    " theorem Integer.sign_of_non_zero_modF is "
  	    "    fa(i : Int, j : Int0) i modF j ~= 0 => sign(i modF j) = sign j"
  	    (:optional "")
  	    " op  divC ((i, j) : Int * Int0) infixl 26 : Int = "
  	    "   if i modT j = 0 || sign i ~= sign j then i divT j else i divT j + 1"
  	    (:optional "")
  	    " op  modC ((i, j) : Int * Int0) infixl 26 : Int = i - j * (i divC j)"
  	    (:optional "")
  	    " conjecture Integer.divC_examples_Obligation_subtype is "
  	    "    14 divC 5 = 3 => 11 divC 5 = 3 => true"
  	    (:optional "")
  	    " conjecture Integer.divC_examples_Obligation_subtype0 is "
  	    "    14 divC 5 = 3 => 11 divC 5 = 3 => -(14) divC 5 = -(2) => true"
  	    (:optional "")
  	    " conjecture Integer.divC_examples_Obligation_subtype1 is "
  	    "    14 divC 5 = 3 "
  	    "    => 11 divC 5 = 3 "
  	    "       => -(14) divC 5 = -(2) => -(11) divC 5 = -(2) => -(5) ~= 0"
  	    (:optional "")
  	    " conjecture Integer.divC_examples_Obligation_subtype2 is "
  	    "    14 divC 5 = 3 "
  	    "    => 11 divC 5 = 3 "
  	    "       => -(14) divC 5 = -(2) "
  	    "          => -(11) divC 5 = -(2) => 14 divC -(5) = -(2) => -(5) ~= 0"
  	    (:optional "")
  	    " conjecture Integer.divC_examples_Obligation_subtype3 is "
  	    "    14 divC 5 = 3 "
  	    "    => 11 divC 5 = 3 "
  	    "       => -(14) divC 5 = -(2) "
  	    "          => -(11) divC 5 = -(2) "
  	    "             => 14 divC -(5) = -(2) => 11 divC -(5) = -(2) => -(5) ~= 0"
  	    (:optional "")
  	    " conjecture Integer.divC_examples_Obligation_subtype4 is "
  	    "    14 divC 5 = 3 "
  	    "    => 11 divC 5 = 3 "
  