--- 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"
--- 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 *}
--- 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"