# HG changeset patch
# User krauss
# Date 1251743688 -7200
# Node ID 3a0a65ca2261178c0fb878b8361e6012e4987ecf
# Parent  c33faa2895202ed352e4cf8ba9832fa4a9a9507e
moved lemma Wellfounded.in_inv_image to Relation.thy

diff -r c33faa289520 -r 3a0a65ca2261 NEWS
--- a/NEWS	Mon Aug 31 20:34:44 2009 +0200
+++ b/NEWS	Mon Aug 31 20:34:48 2009 +0200
@@ -112,6 +112,9 @@
 Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
 Suc_plus1 -> Suc_eq_plus1
 
+* Moved theorems:
+Wellfounded.in_inv_image -> Relation.in_inv_image
+
 * 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"
diff -r c33faa289520 -r 3a0a65ca2261 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Aug 31 20:34:44 2009 +0200
+++ b/src/HOL/Relation.thy	Mon Aug 31 20:34:48 2009 +0200
@@ -599,6 +599,9 @@
   apply blast
   done
 
+lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
+  by (auto simp:inv_image_def)
+
 
 subsection {* Finiteness *}
 
diff -r c33faa289520 -r 3a0a65ca2261 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Aug 31 20:34:44 2009 +0200
+++ b/src/HOL/Wellfounded.thy	Mon Aug 31 20:34:48 2009 +0200
@@ -630,9 +630,6 @@
 apply blast
 done
 
-lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
-  by (auto simp:inv_image_def)
-
 text {* Measure Datatypes into @{typ nat} *}
 
 definition measure :: "('a => nat) => ('a * 'a)set"