anchor.diff:  	    "    apply(rule zgcd_geq_zero)"
   	    "    apply(simp add: zgcd_greatest_iff)"
   	    "  end-proof"
  -	    " "
  +	    (:optional "")
   	    " proof Isa gcd_Obligation_the"
   	    "   apply(rule_tac a=\"zgcd(x,y)\" in ex1I, auto)"
   	    "   (*** similar proof ***) "
  
positive.code: 	    "          => -(11) modE 5 = 4 "
  	    "             => 14 modE -(5) = 4 "
  	    "                => 11 modE -(5) = 1 => -(14) modE -(5) = 1 => -(5) ~= 0"
  	    " "
  	    " theorem Integer.modE_examples is "
  	    "    14 modE 5 = 4 "
  	    "    && 11 modE 5 = 1 "
  
negative.code: 	    "             && 14 divF -(5) = -(3) "
  	    "                && 11 divF -(5) = -(3) "
  	    "                   && -(14) divF -(5) = 2 && -(11) divF -(5) = 2"
  	    (:optional "")
  	    " conjecture Integer.modF_examples_Obligation_subtype is "
  	    "    14 modF 5 = 4 => 11 modF 5 = 1 => true"
  	    (:optional "")
  	    " conjecture Integer.modF_examples_Obligation_subtype0 is "
  	    "    14 modF 5 = 4 => 11 modF 5 = 1 => -(14) modF 5 = 1 => true"
  	    (:optional "")
  	    " conjecture Integer.modF_examples_Obligation_subtype1 is "
  	    "    14 modF 5 = 4 "
  	    "    => 11 modF 5 = 1 => -(14) modF 5 = 1 => -(11) modF 5 = 4 => -(5) ~= 0"
  	    (:optional "")
  	    " conjecture Integer.modF_examples_Obligation_subtype2 is "
  	    "    14 modF 5 = 4 "
  	    "    => 11 modF 5 = 1 "
  	    "       => -(14) modF 5 = 1 "
  	    "          => -(11) modF 5 = 4 => 14 modF -(5) = -(1) => -(5) ~= 0"
  	    (:optional "")
  	    " conjecture Integer.modF_examples_Obligation_subtype3 is "
  	    "    14 modF 5 = 4 "
  	    "    => 11 modF 5 = 1 "
  	    "       => -(14) modF 5 = 1 "
  	    "          => -(11) modF 5 = 4 "
  	    "             => 14 modF -(5) = -(1) => 11 modF -(5) = -(4) => -(5) ~= 0"
  	    (:optional "")
  	    " conjecture Integer.modF_examples_Obligation_subtype4 is "
  	    "    14 modF 5 = 4 "
  	    "    => 11 modF 5 = 1 "
  