--- a/NEWS Fri Jun 26 10:46:33 2009 +0200
+++ b/NEWS Fri Jun 26 19:44:39 2009 +0200
@@ -48,6 +48,10 @@
Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
Suc_plus1 -> Suc_eq_plus1
+* New sledgehammer option "Full Types" in Proof General settings menu.
+Causes full type information to be output to the ATPs. This slows ATPs down
+considerably but eliminates a source of unsound "proofs" that fail later.
+
* Discontinued ancient tradition to suffix certain ML module names with "_package", e.g.:
DatatypePackage ~> Datatype
--- a/src/HOL/GCD.thy Fri Jun 26 10:46:33 2009 +0200
+++ b/src/HOL/GCD.thy Fri Jun 26 19:44:39 2009 +0200
@@ -214,6 +214,15 @@
lemma int_lcm_abs: "lcm (x::int) y = lcm (abs x) (abs y)"
by (simp add: lcm_int_def)
+lemma abs_lcm_int [simp]: "abs (lcm i j::int) = lcm i j"
+by(simp add:lcm_int_def)
+
+lemma lcm_abs1_int[simp]: "lcm (abs x) (y::int) = lcm x y"
+by (metis abs_idempotent lcm_int_def)
+
+lemma lcm_abs2_int[simp]: "lcm x (abs y::int) = lcm x y"
+by (metis abs_idempotent lcm_int_def)
+
lemma int_lcm_cases:
fixes x :: int and y
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"