# HG changeset patch
# User nipkow
# Date 1246038279 -7200
# Node ID 7c122634da818ae408b08681a594c8d46c05bbd7
# Parent  4df828bbc41144a18e4e62a1e575a2bd09903105
lcm abs lemmas

diff -r 4df828bbc411 -r 7c122634da81 NEWS
--- 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
diff -r 4df828bbc411 -r 7c122634da81 src/HOL/GCD.thy
--- 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)"