# HG changeset patch
# User boehmes
# Date 1256197829 -7200
# Node ID d1c9bf0f8ae8e22768dcd7f53b00c960c72d7b4f
# Parent  70f5c18e975d7a13949ddb2ff984c9216c3c8ea3# Parent  764547b6853881f66f2f8fc1f88ecd127249f5ee
merged

diff -r 70f5c18e975d -r d1c9bf0f8ae8 NEWS
--- a/NEWS	Thu Oct 22 09:49:48 2009 +0200
+++ b/NEWS	Thu Oct 22 09:50:29 2009 +0200
@@ -153,8 +153,8 @@
 this.  Fix using O_assoc[symmetric].  The same applies to the curried
 version "R OO S".
 
-* Function "Inv" is renamed to "inv_onto" and function "inv" is now an
-abbreviation for "inv_onto UNIV". Lemmas are renamed accordingly.
+* Function "Inv" is renamed to "inv_into" and function "inv" is now an
+abbreviation for "inv_into UNIV". Lemmas are renamed accordingly.
 INCOMPATIBILITY.
 
 * ML antiquotation @{code_datatype} inserts definition of a datatype
diff -r 70f5c18e975d -r d1c9bf0f8ae8 doc-src/Main/Docs/Main_Doc.thy
--- a/doc-src/Main/Docs/Main_Doc.thy	Thu Oct 22 09:49:48 2009 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy	Thu Oct 22 09:50:29 2009 +0200
@@ -170,13 +170,13 @@
 \smallskip
 
 \begin{tabular}{@ {} l @ {~::~} l @ {}}
-@{const Hilbert_Choice.inv_onto} & @{term_type_only Hilbert_Choice.inv_onto "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"}
+@{const Hilbert_Choice.inv_into} & @{term_type_only Hilbert_Choice.inv_into "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"}
 \end{tabular}
 
 \subsubsection*{Syntax}
 
 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-@{term inv} & @{term[source]"inv_onto UNIV"}
+@{term inv} & @{term[source]"inv_into UNIV"}
 \end{tabular}
 
 \section{Fixed Points}
diff -r 70f5c18e975d -r d1c9bf0f8ae8 doc-src/Main/Docs/document/Main_Doc.tex
--- a/doc-src/Main/Docs/document/Main_Doc.tex	Thu Oct 22 09:49:48 2009 +0200
+++ b/doc-src/Main/Docs/document/Main_Doc.tex	Thu Oct 22 09:50:29 2009 +0200
@@ -181,13 +181,13 @@
 \smallskip
 
 \begin{tabular}{@ {} l @ {~::~} l @ {}}
-\isa{inv{\isacharunderscore}onto} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a}
+\isa{inv{\isacharunderscore}into} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a}
 \end{tabular}
 
 \subsubsection*{Syntax}
 
 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-\isa{inv} & \isa{{\isachardoublequote}inv{\isacharunderscore}onto\ UNIV{\isachardoublequote}}
+\isa{inv} & \isa{{\isachardoublequote}inv{\isacharunderscore}into\ UNIV{\isachardoublequote}}
 \end{tabular}
 
 \section{Fixed Points}
diff -r 70f5c18e975d -r d1c9bf0f8ae8 doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Thu Oct 22 09:49:48 2009 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex	Thu Oct 22 09:50:29 2009 +0200
@@ -1357,7 +1357,7 @@
 some $x$ such that $P(x)$ is true, provided one exists.
 Isabelle uses \sdx{SOME} for the Greek letter~$\varepsilon$.
 
-Here is the definition of~\cdx{inv},\footnote{In fact, \isa{inv} is defined via a second constant \isa{inv_onto}, which we ignore here.} which expresses inverses of
+Here is the definition of~\cdx{inv},\footnote{In fact, \isa{inv} is defined via a second constant \isa{inv_into}, which we ignore here.} which expresses inverses of
 functions:
 \begin{isabelle}
 inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y%
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Algebra/Bij.thy
--- a/src/HOL/Algebra/Bij.thy	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Algebra/Bij.thy	Thu Oct 22 09:50:29 2009 +0200
@@ -31,8 +31,8 @@
 
 subsection {*Bijections Form a Group *}
 
-lemma restrict_inv_onto_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (inv_onto S f) x) \<in> Bij S"
-  by (simp add: Bij_def bij_betw_inv_onto)
+lemma restrict_inv_into_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (inv_into S f) x) \<in> Bij S"
+  by (simp add: Bij_def bij_betw_inv_into)
 
 lemma id_Bij: "(\<lambda>x\<in>S. x) \<in> Bij S "
   by (auto simp add: Bij_def bij_betw_def inj_on_def)
@@ -41,8 +41,8 @@
   by (auto simp add: Bij_def bij_betw_compose) 
 
 lemma Bij_compose_restrict_eq:
-     "f \<in> Bij S \<Longrightarrow> compose S (restrict (inv_onto S f) S) f = (\<lambda>x\<in>S. x)"
-  by (simp add: Bij_def compose_inv_onto_id)
+     "f \<in> Bij S \<Longrightarrow> compose S (restrict (inv_into S f) S) f = (\<lambda>x\<in>S. x)"
+  by (simp add: Bij_def compose_inv_into_id)
 
 theorem group_BijGroup: "group (BijGroup S)"
 apply (simp add: BijGroup_def)
@@ -52,19 +52,19 @@
   apply (simp add: compose_Bij)
   apply (blast intro: compose_assoc [symmetric] dest: Bij_imp_funcset)
  apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp)
-apply (blast intro: Bij_compose_restrict_eq restrict_inv_onto_Bij)
+apply (blast intro: Bij_compose_restrict_eq restrict_inv_into_Bij)
 done
 
 
 subsection{*Automorphisms Form a Group*}
 
-lemma Bij_inv_onto_mem: "\<lbrakk> f \<in> Bij S;  x \<in> S\<rbrakk> \<Longrightarrow> inv_onto S f x \<in> S"
-by (simp add: Bij_def bij_betw_def inv_onto_into)
+lemma Bij_inv_into_mem: "\<lbrakk> f \<in> Bij S;  x \<in> S\<rbrakk> \<Longrightarrow> inv_into S f x \<in> S"
+by (simp add: Bij_def bij_betw_def inv_into_into)
 
-lemma Bij_inv_onto_lemma:
+lemma Bij_inv_into_lemma:
  assumes eq: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> h(g x y) = g (h x) (h y)"
  shows "\<lbrakk>h \<in> Bij S;  g \<in> S \<rightarrow> S \<rightarrow> S;  x \<in> S;  y \<in> S\<rbrakk>
-        \<Longrightarrow> inv_onto S h (g x y) = g (inv_onto S h x) (inv_onto S h y)"
+        \<Longrightarrow> inv_into S h (g x y) = g (inv_into S h x) (inv_into S h y)"
 apply (simp add: Bij_def bij_betw_def)
 apply (subgoal_tac "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' & y = h y'", clarify)
  apply (simp add: eq [symmetric] inv_f_f funcset_mem [THEN funcset_mem], blast)
@@ -84,17 +84,17 @@
 lemma (in group) mult_funcset: "mult G \<in> carrier G \<rightarrow> carrier G \<rightarrow> carrier G"
   by (simp add:  Pi_I group.axioms)
 
-lemma (in group) restrict_inv_onto_hom:
+lemma (in group) restrict_inv_into_hom:
       "\<lbrakk>h \<in> hom G G; h \<in> Bij (carrier G)\<rbrakk>
-       \<Longrightarrow> restrict (inv_onto (carrier G) h) (carrier G) \<in> hom G G"
-  by (simp add: hom_def Bij_inv_onto_mem restrictI mult_funcset
-                group.axioms Bij_inv_onto_lemma)
+       \<Longrightarrow> restrict (inv_into (carrier G) h) (carrier G) \<in> hom G G"
+  by (simp add: hom_def Bij_inv_into_mem restrictI mult_funcset
+                group.axioms Bij_inv_into_lemma)
 
 lemma inv_BijGroup:
-     "f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (inv_onto S f) x)"
+     "f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (inv_into S f) x)"
 apply (rule group.inv_equality)
 apply (rule group_BijGroup)
-apply (simp_all add:BijGroup_def restrict_inv_onto_Bij Bij_compose_restrict_eq)
+apply (simp_all add:BijGroup_def restrict_inv_into_Bij Bij_compose_restrict_eq)
 done
 
 lemma (in group) subgroup_auto:
@@ -115,7 +115,7 @@
   assume "x \<in> auto G" 
   thus "inv\<^bsub>BijGroup (carrier G)\<^esub> x \<in> auto G"
     by (simp del: restrict_apply
-        add: inv_BijGroup auto_def restrict_inv_onto_Bij restrict_inv_onto_hom)
+        add: inv_BijGroup auto_def restrict_inv_into_Bij restrict_inv_into_hom)
 qed
 
 theorem (in group) AutoGroup: "group (AutoGroup G)"
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Algebra/Group.thy	Thu Oct 22 09:50:29 2009 +0200
@@ -553,11 +553,11 @@
 by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
 
 lemma (in group) iso_sym:
-     "h \<in> G \<cong> H \<Longrightarrow> inv_onto (carrier G) h \<in> H \<cong> G"
-apply (simp add: iso_def bij_betw_inv_onto) 
-apply (subgoal_tac "inv_onto (carrier G) h \<in> carrier H \<rightarrow> carrier G") 
- prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_onto]) 
-apply (simp add: hom_def bij_betw_def inv_onto_f_eq f_inv_onto_f Pi_def)
+     "h \<in> G \<cong> H \<Longrightarrow> inv_into (carrier G) h \<in> H \<cong> G"
+apply (simp add: iso_def bij_betw_inv_into) 
+apply (subgoal_tac "inv_into (carrier G) h \<in> carrier H \<rightarrow> carrier G") 
+ prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_into]) 
+apply (simp add: hom_def bij_betw_def inv_into_f_eq f_inv_into_f Pi_def)
 done
 
 lemma (in group) iso_trans: 
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Oct 22 09:50:29 2009 +0200
@@ -162,9 +162,9 @@
   from finite_imp_nat_seg_image_inj_on[OF `finite A`]
   obtain f and n::nat where bij: "bij_betw f {i. i<n} A"
     by (auto simp:bij_betw_def)
-  let ?f = "the_inv_onto {i. i<n} f"
+  let ?f = "the_inv_into {i. i<n} f"
   have "inj_on ?f A & ?f ` A = {i. i<n}"
-    by (fold bij_betw_def) (rule bij_betw_the_inv_onto[OF bij])
+    by (fold bij_betw_def) (rule bij_betw_the_inv_into[OF bij])
   thus ?thesis by blast
 qed
 
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Fun.thy	Thu Oct 22 09:50:29 2009 +0200
@@ -508,65 +508,65 @@
 
 subsection {* Inversion of injective functions *}
 
-definition the_inv_onto :: "'a set => ('a => 'b) => ('b => 'a)" where
-"the_inv_onto A f == %x. THE y. y : A & f y = x"
+definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
+"the_inv_into A f == %x. THE y. y : A & f y = x"
 
-lemma the_inv_onto_f_f:
-  "[| inj_on f A;  x : A |] ==> the_inv_onto A f (f x) = x"
-apply (simp add: the_inv_onto_def inj_on_def)
+lemma the_inv_into_f_f:
+  "[| inj_on f A;  x : A |] ==> the_inv_into A f (f x) = x"
+apply (simp add: the_inv_into_def inj_on_def)
 apply (blast intro: the_equality)
 done
 
-lemma f_the_inv_onto_f:
-  "inj_on f A ==> y : f`A  ==> f (the_inv_onto A f y) = y"
-apply (simp add: the_inv_onto_def)
+lemma f_the_inv_into_f:
+  "inj_on f A ==> y : f`A  ==> f (the_inv_into A f y) = y"
+apply (simp add: the_inv_into_def)
 apply (rule the1I2)
  apply(blast dest: inj_onD)
 apply blast
 done
 
-lemma the_inv_onto_into:
-  "[| inj_on f A; x : f ` A; A <= B |] ==> the_inv_onto A f x : B"
-apply (simp add: the_inv_onto_def)
+lemma the_inv_into_into:
+  "[| inj_on f A; x : f ` A; A <= B |] ==> the_inv_into A f x : B"
+apply (simp add: the_inv_into_def)
 apply (rule the1I2)
  apply(blast dest: inj_onD)
 apply blast
 done
 
-lemma the_inv_onto_onto[simp]:
-  "inj_on f A ==> the_inv_onto A f ` (f ` A) = A"
-by (fast intro:the_inv_onto_into the_inv_onto_f_f[symmetric])
+lemma the_inv_into_onto[simp]:
+  "inj_on f A ==> the_inv_into A f ` (f ` A) = A"
+by (fast intro:the_inv_into_into the_inv_into_f_f[symmetric])
 
-lemma the_inv_onto_f_eq:
-  "[| inj_on f A; f x = y; x : A |] ==> the_inv_onto A f y = x"
+lemma the_inv_into_f_eq:
+  "[| inj_on f A; f x = y; x : A |] ==> the_inv_into A f y = x"
   apply (erule subst)
-  apply (erule the_inv_onto_f_f, assumption)
+  apply (erule the_inv_into_f_f, assumption)
   done
 
-lemma the_inv_onto_comp:
+lemma the_inv_into_comp:
   "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==>
-  the_inv_onto A (f o g) x = (the_inv_onto A g o the_inv_onto (g ` A) f) x"
-apply (rule the_inv_onto_f_eq)
+  the_inv_into A (f o g) x = (the_inv_into A g o the_inv_into (g ` A) f) x"
+apply (rule the_inv_into_f_eq)
   apply (fast intro: comp_inj_on)
- apply (simp add: f_the_inv_onto_f the_inv_onto_into)
-apply (simp add: the_inv_onto_into)
+ apply (simp add: f_the_inv_into_f the_inv_into_into)
+apply (simp add: the_inv_into_into)
 done
 
-lemma inj_on_the_inv_onto:
-  "inj_on f A \<Longrightarrow> inj_on (the_inv_onto A f) (f ` A)"
-by (auto intro: inj_onI simp: image_def the_inv_onto_f_f)
+lemma inj_on_the_inv_into:
+  "inj_on f A \<Longrightarrow> inj_on (the_inv_into A f) (f ` A)"
+by (auto intro: inj_onI simp: image_def the_inv_into_f_f)
 
-lemma bij_betw_the_inv_onto:
-  "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_onto A f) B A"
-by (auto simp add: bij_betw_def inj_on_the_inv_onto the_inv_onto_into)
+lemma bij_betw_the_inv_into:
+  "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_into A f) B A"
+by (auto simp add: bij_betw_def inj_on_the_inv_into the_inv_into_into)
 
 abbreviation the_inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
-  "the_inv f \<equiv> the_inv_onto UNIV f"
+  "the_inv f \<equiv> the_inv_into UNIV f"
 
 lemma the_inv_f_f:
   assumes "inj f"
   shows "the_inv f (f x) = x" using assms UNIV_I
-  by (rule the_inv_onto_f_f)
+  by (rule the_inv_into_f_f)
 
 
 subsection {* Proof tool setup *} 
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/HOL.thy	Thu Oct 22 09:50:29 2009 +0200
@@ -2049,33 +2049,33 @@
 text {* This will be relocated once Nitpick is moved to HOL. *}
 
 ML {*
-structure Nitpick_Const_Defs = Named_Thms
+structure Nitpick_Defs = Named_Thms
 (
-  val name = "nitpick_const_def"
+  val name = "nitpick_def"
   val description = "alternative definitions of constants as needed by Nitpick"
 )
-structure Nitpick_Const_Simps = Named_Thms
+structure Nitpick_Simps = Named_Thms
 (
-  val name = "nitpick_const_simp"
+  val name = "nitpick_simp"
   val description = "equational specification of constants as needed by Nitpick"
 )
-structure Nitpick_Const_Psimps = Named_Thms
+structure Nitpick_Psimps = Named_Thms
 (
-  val name = "nitpick_const_psimp"
+  val name = "nitpick_psimp"
   val description = "partial equational specification of constants as needed by Nitpick"
 )
-structure Nitpick_Ind_Intros = Named_Thms
+structure Nitpick_Intros = Named_Thms
 (
-  val name = "nitpick_ind_intro"
+  val name = "nitpick_intro"
   val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
 )
 *}
 
 setup {*
-  Nitpick_Const_Defs.setup
-  #> Nitpick_Const_Simps.setup
-  #> Nitpick_Const_Psimps.setup
-  #> Nitpick_Ind_Intros.setup
+  Nitpick_Defs.setup
+  #> Nitpick_Simps.setup
+  #> Nitpick_Psimps.setup
+  #> Nitpick_Intros.setup
 *}
 
 
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Thu Oct 22 09:50:29 2009 +0200
@@ -31,11 +31,11 @@
      in Syntax.const "_Eps" $ x $ t end)]
 *}
 
-definition inv_onto :: "'a set => ('a => 'b) => ('b => 'a)" where
-"inv_onto A f == %x. SOME y. y : A & f y = x"
+definition inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
+"inv_into A f == %x. SOME y. y : A & f y = x"
 
 abbreviation inv :: "('a => 'b) => ('b => 'a)" where
-"inv == inv_onto UNIV"
+"inv == inv_into UNIV"
 
 
 subsection {*Hilbert's Epsilon-operator*}
@@ -92,40 +92,40 @@
 subsection {*Function Inverse*}
 
 lemma inv_def: "inv f = (%y. SOME x. f x = y)"
-by(simp add: inv_onto_def)
+by(simp add: inv_into_def)
 
-lemma inv_onto_into: "x : f ` A ==> inv_onto A f x : A"
-apply (simp add: inv_onto_def)
+lemma inv_into_into: "x : f ` A ==> inv_into A f x : A"
+apply (simp add: inv_into_def)
 apply (fast intro: someI2)
 done
 
 lemma inv_id [simp]: "inv id = id"
-by (simp add: inv_onto_def id_def)
+by (simp add: inv_into_def id_def)
 
-lemma inv_onto_f_f [simp]:
-  "[| inj_on f A;  x : A |] ==> inv_onto A f (f x) = x"
-apply (simp add: inv_onto_def inj_on_def)
+lemma inv_into_f_f [simp]:
+  "[| inj_on f A;  x : A |] ==> inv_into A f (f x) = x"
+apply (simp add: inv_into_def inj_on_def)
 apply (blast intro: someI2)
 done
 
 lemma inv_f_f: "inj f ==> inv f (f x) = x"
-by (simp add: inv_onto_f_f)
+by (simp add: inv_into_f_f)
 
-lemma f_inv_onto_f: "y : f`A  ==> f (inv_onto A f y) = y"
-apply (simp add: inv_onto_def)
+lemma f_inv_into_f: "y : f`A  ==> f (inv_into A f y) = y"
+apply (simp add: inv_into_def)
 apply (fast intro: someI2)
 done
 
-lemma inv_onto_f_eq: "[| inj_on f A; x : A; f x = y |] ==> inv_onto A f y = x"
+lemma inv_into_f_eq: "[| inj_on f A; x : A; f x = y |] ==> inv_into A f y = x"
 apply (erule subst)
-apply (fast intro: inv_onto_f_f)
+apply (fast intro: inv_into_f_f)
 done
 
 lemma inv_f_eq: "[| inj f; f x = y |] ==> inv f y = x"
-by (simp add:inv_onto_f_eq)
+by (simp add:inv_into_f_eq)
 
 lemma inj_imp_inv_eq: "[| inj f; ALL x. f(g x) = x |] ==> inv f = g"
-by (blast intro: ext inv_onto_f_eq)
+by (blast intro: ext inv_into_f_eq)
 
 text{*But is it useful?*}
 lemma inj_transfer:
@@ -134,12 +134,12 @@
 proof -
   have "f x \<in> range f" by auto
   hence "P(inv f (f x))" by (rule minor)
-  thus "P x" by (simp add: inv_onto_f_f [OF injf])
+  thus "P x" by (simp add: inv_into_f_f [OF injf])
 qed
 
 lemma inj_iff: "(inj f) = (inv f o f = id)"
 apply (simp add: o_def expand_fun_eq)
-apply (blast intro: inj_on_inverseI inv_onto_f_f)
+apply (blast intro: inj_on_inverseI inv_into_f_f)
 done
 
 lemma inv_o_cancel[simp]: "inj f ==> inv f o f = id"
@@ -148,34 +148,34 @@
 lemma o_inv_o_cancel[simp]: "inj f ==> g o inv f o f = g"
 by (simp add: o_assoc[symmetric])
 
-lemma inv_onto_image_cancel[simp]:
-  "inj_on f A ==> S <= A ==> inv_onto A f ` f ` S = S"
+lemma inv_into_image_cancel[simp]:
+  "inj_on f A ==> S <= A ==> inv_into A f ` f ` S = S"
 by(fastsimp simp: image_def)
 
 lemma inj_imp_surj_inv: "inj f ==> surj (inv f)"
-by (blast intro: surjI inv_onto_f_f)
+by (blast intro: surjI inv_into_f_f)
 
 lemma surj_f_inv_f: "surj f ==> f(inv f y) = y"
-by (simp add: f_inv_onto_f surj_range)
+by (simp add: f_inv_into_f surj_range)
 
-lemma inv_onto_injective:
-  assumes eq: "inv_onto A f x = inv_onto A f y"
+lemma inv_into_injective:
+  assumes eq: "inv_into A f x = inv_into A f y"
       and x: "x: f`A"
       and y: "y: f`A"
   shows "x=y"
 proof -
-  have "f (inv_onto A f x) = f (inv_onto A f y)" using eq by simp
-  thus ?thesis by (simp add: f_inv_onto_f x y)
+  have "f (inv_into A f x) = f (inv_into A f y)" using eq by simp
+  thus ?thesis by (simp add: f_inv_into_f x y)
 qed
 
-lemma inj_on_inv_onto: "B <= f`A ==> inj_on (inv_onto A f) B"
-by (blast intro: inj_onI dest: inv_onto_injective injD)
+lemma inj_on_inv_into: "B <= f`A ==> inj_on (inv_into A f) B"
+by (blast intro: inj_onI dest: inv_into_injective injD)
 
-lemma bij_betw_inv_onto: "bij_betw f A B ==> bij_betw (inv_onto A f) B A"
-by (auto simp add: bij_betw_def inj_on_inv_onto)
+lemma bij_betw_inv_into: "bij_betw f A B ==> bij_betw (inv_into A f) B A"
+by (auto simp add: bij_betw_def inj_on_inv_into)
 
 lemma surj_imp_inj_inv: "surj f ==> inj (inv f)"
-by (simp add: inj_on_inv_onto surj_range)
+by (simp add: inj_on_inv_into surj_range)
 
 lemma surj_iff: "(surj f) = (f o inv f = id)"
 apply (simp add: o_def expand_fun_eq)
@@ -193,7 +193,7 @@
 
 lemma inv_equality: "[| !!x. g (f x) = x;  !!y. f (g y) = y |] ==> inv f = g"
 apply (rule ext)
-apply (auto simp add: inv_onto_def)
+apply (auto simp add: inv_into_def)
 done
 
 lemma inv_inv_eq: "bij f ==> inv (inv f) = f"
@@ -208,13 +208,13 @@
     inv(inv f)=f all fail.
 **)
 
-lemma inv_onto_comp:
+lemma inv_into_comp:
   "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==>
-  inv_onto A (f o g) x = (inv_onto A g o inv_onto (g ` A) f) x"
-apply (rule inv_onto_f_eq)
+  inv_into A (f o g) x = (inv_into A g o inv_into (g ` A) f) x"
+apply (rule inv_into_f_eq)
   apply (fast intro: comp_inj_on)
- apply (simp add: inv_onto_into)
-apply (simp add: f_inv_onto_f inv_onto_into)
+ apply (simp add: inv_into_into)
+apply (simp add: f_inv_into_f inv_into_into)
 done
 
 lemma o_inv_distrib: "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f"
@@ -239,7 +239,7 @@
 
 lemma bij_vimage_eq_inv_image: "bij f ==> f -` A = inv f ` A" 
 apply (auto simp add: bij_is_surj [THEN surj_f_inv_f])
-apply (blast intro: bij_is_inj [THEN inv_onto_f_f, symmetric])
+apply (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric])
 done
 
 lemma finite_fun_UNIVD1:
@@ -256,7 +256,7 @@
   moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
   proof (rule UNIV_eq_I)
     fix x :: 'a
-    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_onto_def)
+    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_into_def)
     thus "x \<in> range (\<lambda>f\<Colon>'a \<Rightarrow> 'b. inv f b1)" by blast
   qed
   ultimately show "finite (UNIV :: 'a set)" by simp
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Induct/LList.thy
--- a/src/HOL/Induct/LList.thy	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Induct/LList.thy	Thu Oct 22 09:50:29 2009 +0200
@@ -665,7 +665,7 @@
 apply (subst LList_corec, force)
 done
 
-lemma llist_corec [nitpick_const_simp]: 
+lemma llist_corec [nitpick_simp]: 
     "llist_corec a f =   
      (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))"
 apply (unfold llist_corec_def LNil_def LCons_def)
@@ -774,10 +774,10 @@
 
 subsection{* The functional @{text lmap} *}
 
-lemma lmap_LNil [simp, nitpick_const_simp]: "lmap f LNil = LNil"
+lemma lmap_LNil [simp, nitpick_simp]: "lmap f LNil = LNil"
 by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
 
-lemma lmap_LCons [simp, nitpick_const_simp]:
+lemma lmap_LCons [simp, nitpick_simp]:
 "lmap f (LCons M N) = LCons (f M) (lmap f N)"
 by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
 
@@ -793,7 +793,7 @@
 
 subsection{* iterates -- @{text llist_fun_equalityI} cannot be used! *}
 
-lemma iterates [nitpick_const_simp]: "iterates f x = LCons x (iterates f (f x))"
+lemma iterates [nitpick_simp]: "iterates f x = LCons x (iterates f (f x))"
 by (rule iterates_def [THEN def_llist_corec, THEN trans], simp)
 
 lemma lmap_iterates [simp]: "lmap f (iterates f x) = iterates f (f x)"
@@ -848,18 +848,18 @@
 
 subsection{* @{text lappend} -- its two arguments cause some complications! *}
 
-lemma lappend_LNil_LNil [simp, nitpick_const_simp]: "lappend LNil LNil = LNil"
+lemma lappend_LNil_LNil [simp, nitpick_simp]: "lappend LNil LNil = LNil"
 apply (simp add: lappend_def)
 apply (rule llist_corec [THEN trans], simp)
 done
 
-lemma lappend_LNil_LCons [simp, nitpick_const_simp]: 
+lemma lappend_LNil_LCons [simp, nitpick_simp]: 
     "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
 apply (simp add: lappend_def)
 apply (rule llist_corec [THEN trans], simp)
 done
 
-lemma lappend_LCons [simp, nitpick_const_simp]: 
+lemma lappend_LCons [simp, nitpick_simp]: 
     "lappend (LCons l l') N = LCons l (lappend l' N)"
 apply (simp add: lappend_def)
 apply (rule llist_corec [THEN trans], simp)
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Int.thy	Thu Oct 22 09:50:29 2009 +0200
@@ -1614,7 +1614,7 @@
 context ring_1
 begin
 
-lemma of_int_of_nat [nitpick_const_simp]:
+lemma of_int_of_nat [nitpick_simp]:
   "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
 proof (cases "k < 0")
   case True then have "0 \<le> - k" by simp
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Library/Coinductive_List.thy
--- a/src/HOL/Library/Coinductive_List.thy	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Library/Coinductive_List.thy	Thu Oct 22 09:50:29 2009 +0200
@@ -260,7 +260,7 @@
   qed
 qed
 
-lemma llist_corec [code, nitpick_const_simp]:
+lemma llist_corec [code, nitpick_simp]:
   "llist_corec a f =
     (case f a of None \<Rightarrow> LNil | Some (z, w) \<Rightarrow> LCons z (llist_corec w f))"
 proof (cases "f a")
@@ -656,8 +656,8 @@
   qed
 qed
 
-lemma lmap_LNil [simp, nitpick_const_simp]: "lmap f LNil = LNil"
-  and lmap_LCons [simp, nitpick_const_simp]:
+lemma lmap_LNil [simp, nitpick_simp]: "lmap f LNil = LNil"
+  and lmap_LCons [simp, nitpick_simp]:
   "lmap f (LCons M N) = LCons (f M) (lmap f N)"
   by (simp_all add: lmap_def llist_corec)
 
@@ -729,9 +729,9 @@
   qed
 qed
 
-lemma lappend_LNil_LNil [simp, nitpick_const_simp]: "lappend LNil LNil = LNil"
-  and lappend_LNil_LCons [simp, nitpick_const_simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
-  and lappend_LCons [simp, nitpick_const_simp]: "lappend (LCons l l') m = LCons l (lappend l' m)"
+lemma lappend_LNil_LNil [simp, nitpick_simp]: "lappend LNil LNil = LNil"
+  and lappend_LNil_LCons [simp, nitpick_simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
+  and lappend_LCons [simp, nitpick_simp]: "lappend (LCons l l') m = LCons l (lappend l' m)"
   by (simp_all add: lappend_def llist_corec)
 
 lemma lappend_LNil1 [simp]: "lappend LNil l = l"
@@ -755,7 +755,7 @@
   iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
   "iterates f a = llist_corec a (\<lambda>x. Some (x, f x))"
 
-lemma iterates [nitpick_const_simp]: "iterates f x = LCons x (iterates f (f x))"
+lemma iterates [nitpick_simp]: "iterates f x = LCons x (iterates f (f x))"
   apply (unfold iterates_def)
   apply (subst llist_corec)
   apply simp
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Library/FuncSet.thy	Thu Oct 22 09:50:29 2009 +0200
@@ -190,20 +190,20 @@
       !!x. x\<in>A ==> f x = g x |] ==> f = g"
 by (force simp add: expand_fun_eq extensional_def)
 
-lemma inv_onto_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_onto A f x) : B -> A"
-by (unfold inv_onto_def) (fast intro: someI2)
+lemma inv_into_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_into A f x) : B -> A"
+by (unfold inv_into_def) (fast intro: someI2)
 
-lemma compose_inv_onto_id:
-  "bij_betw f A B ==> compose A (\<lambda>y\<in>B. inv_onto A f y) f = (\<lambda>x\<in>A. x)"
+lemma compose_inv_into_id:
+  "bij_betw f A B ==> compose A (\<lambda>y\<in>B. inv_into A f y) f = (\<lambda>x\<in>A. x)"
 apply (simp add: bij_betw_def compose_def)
 apply (rule restrict_ext, auto)
 done
 
-lemma compose_id_inv_onto:
-  "f ` A = B ==> compose B f (\<lambda>y\<in>B. inv_onto A f y) = (\<lambda>x\<in>B. x)"
+lemma compose_id_inv_into:
+  "f ` A = B ==> compose B f (\<lambda>y\<in>B. inv_into A f y) = (\<lambda>x\<in>B. x)"
 apply (simp add: compose_def)
 apply (rule restrict_ext)
-apply (simp add: f_inv_onto_f)
+apply (simp add: f_inv_into_f)
 done
 
 
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Library/Permutations.thy	Thu Oct 22 09:50:29 2009 +0200
@@ -83,7 +83,7 @@
   unfolding permutes_def by simp
 
 lemma permutes_inv_eq: "p permutes S ==> inv p y = x \<longleftrightarrow> p x = y"
-  unfolding permutes_def inv_onto_def apply auto
+  unfolding permutes_def inv_def apply auto
   apply (erule allE[where x=y])
   apply (erule allE[where x=y])
   apply (rule someI_ex) apply blast
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Oct 22 09:50:29 2009 +0200
@@ -372,8 +372,7 @@
          in
            lthy''
            |> LocalTheory.note Thm.generatedK ((qualify (Binding.name "simps"),
-                map (Attrib.internal o K)
-                    [Simplifier.simp_add, Nitpick_Const_Simps.add]),
+                map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]),
                 maps snd simps')
            |> snd
          end)
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/SizeChange/Correctness.thy
--- a/src/HOL/SizeChange/Correctness.thy	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/SizeChange/Correctness.thy	Thu Oct 22 09:50:29 2009 +0200
@@ -1146,7 +1146,7 @@
   assumes "finite S" 
   shows "set (set2list S) = S"
   unfolding set2list_def 
-proof (rule f_inv_onto_f)
+proof (rule f_inv_into_f)
   from `finite S` have "\<exists>l. set l = S"
     by (rule finite_list)
   thus "S \<in> range set"
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 22 09:50:29 2009 +0200
@@ -262,8 +262,7 @@
   in
     thy2
     |> Sign.add_path (space_implode "_" new_type_names)
-    |> PureThy.add_thmss [((Binding.name "recs", rec_thms),
-         [Nitpick_Const_Simps.add])]
+    |> PureThy.add_thmss [((Binding.name "recs", rec_thms), [Nitpick_Simps.add])]
     ||> Sign.parent_path
     ||> Theory.checkpoint
     |-> (fn thms => pair (reccomb_names, flat thms))
@@ -335,7 +334,7 @@
           (DatatypeProp.make_cases new_type_names descr sorts thy2)
   in
     thy2
-    |> Context.the_theory o fold (fold Nitpick_Const_Simps.add_thm) case_thms
+    |> Context.the_theory o fold (fold Nitpick_Simps.add_thm) case_thms
        o Context.Theory
     |> Sign.parent_path
     |> store_thmss "cases" new_type_names case_thms
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Tools/Datatype/datatype_rep_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Thu Oct 22 09:50:29 2009 +0200
@@ -481,7 +481,7 @@
 
     val Abs_inverse_thms' =
       map #1 newT_iso_axms @
-      map2 (fn r_inj => fn r => @{thm f_the_inv_onto_f} OF [r_inj, r RS mp])
+      map2 (fn r_inj => fn r => @{thm f_the_inv_into_f} OF [r_inj, r RS mp])
         iso_inj_thms_unfolded iso_thms;
 
     val Abs_inverse_thms = maps (mk_funs_inv thy5) Abs_inverse_thms';
@@ -571,7 +571,7 @@
         val Abs_t = if i < length newTs then
             Const (Sign.intern_const thy6
               ("Abs_" ^ (nth new_type_names i)), Univ_elT --> T)
-          else Const (@{const_name the_inv_onto},
+          else Const (@{const_name the_inv_into},
               [HOLogic.mk_setT T, T --> Univ_elT, Univ_elT] ---> T) $
             HOLogic.mk_UNIV T $ Const (nth all_rep_names i, T --> Univ_elT)
 
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Tools/Function/fundef.ML
--- a/src/HOL/Tools/Function/fundef.ML	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Tools/Function/fundef.ML	Thu Oct 22 09:50:29 2009 +0200
@@ -37,12 +37,12 @@
 val simp_attribs = map (Attrib.internal o K)
     [Simplifier.simp_add,
      Code.add_default_eqn_attribute,
-     Nitpick_Const_Simps.add,
+     Nitpick_Simps.add,
      Quickcheck_RecFun_Simps.add]
 
 val psimp_attribs = map (Attrib.internal o K)
     [Simplifier.simp_add,
-     Nitpick_Const_Psimps.add]
+     Nitpick_Psimps.add]
 
 fun note_theorem ((name, atts), ths) =
   LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths)
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Tools/Function/size.ML	Thu Oct 22 09:50:29 2009 +0200
@@ -209,7 +209,7 @@
 
     val ([size_thms], thy'') =  PureThy.add_thmss
       [((Binding.name "size", size_eqns),
-        [Simplifier.simp_add, Nitpick_Const_Simps.add,
+        [Simplifier.simp_add, Nitpick_Simps.add,
          Thm.declaration_attribute
              (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
 
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Tools/Predicate_Compile/pred_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Thu Oct 22 09:50:29 2009 +0200
@@ -157,7 +157,7 @@
 
 fun make_const_spec_table thy =
   fold store_thm (Predicate_Compile_Preproc_Const_Defs.get (ProofContext.init thy)) thy
-  |> (fn thy => fold store_thm (Nitpick_Const_Simps.get (ProofContext.init thy)) thy)
+  |> (fn thy => fold store_thm (Nitpick_Simps.get (ProofContext.init thy)) thy)
 *)
 fun make_const_spec_table thy =
   let
@@ -168,8 +168,8 @@
   in
     table   
     |> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get
-    |> store ignore_consts Nitpick_Const_Simps.get
-    |> store ignore_consts Nitpick_Ind_Intros.get
+    |> store ignore_consts Nitpick_Simps.get
+    |> store ignore_consts Nitpick_Intros.get
   end
   (*
 fun get_specification thy constname =
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Thu Oct 22 09:50:29 2009 +0200
@@ -703,7 +703,7 @@
       LocalTheory.notes kind
         (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
            [Attrib.internal (K (ContextRules.intro_query NONE)),
-            Attrib.internal (K Nitpick_Ind_Intros.add)])]) intrs) |>>
+            Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>>
       map (hd o snd);
     val (((_, elims'), (_, [induct'])), ctxt2) =
       ctxt1 |>
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Tools/old_primrec.ML
--- a/src/HOL/Tools/old_primrec.ML	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML	Thu Oct 22 09:50:29 2009 +0200
@@ -284,7 +284,7 @@
   in
     thy''
     |> note (("simps",
-        [Simplifier.simp_add, Nitpick_Const_Simps.add, Code.add_default_eqn_attribute]), simps'')
+        [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]), simps'')
     |> snd
     |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
     |> snd
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Tools/primrec.ML	Thu Oct 22 09:50:29 2009 +0200
@@ -272,7 +272,7 @@
       (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec;
     fun simp_attr_binding prefix = (Binding.qualify true prefix (Binding.name "simps"),
       map (Attrib.internal o K)
-        [Simplifier.simp_add, Nitpick_Const_Simps.add, Quickcheck_RecFun_Simps.add]);
+        [Simplifier.simp_add, Nitpick_Simps.add, Quickcheck_RecFun_Simps.add]);
   in
     lthy
     |> set_group ? LocalTheory.set_group (serial_string ())
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Oct 22 09:50:29 2009 +0200
@@ -214,7 +214,7 @@
     |-> (fn proto_simps => prove_simps proto_simps)
     |-> (fn simps => LocalTheory.note Thm.generatedK ((b,
            Code.add_default_eqn_attrib :: map (Attrib.internal o K)
-          [Simplifier.simp_add, Nitpick_Const_Simps.add, Quickcheck_RecFun_Simps.add]),
+          [Simplifier.simp_add, Nitpick_Simps.add, Quickcheck_RecFun_Simps.add]),
             simps))
     |> snd
   end
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Tools/recdef.ML	Thu Oct 22 09:50:29 2009 +0200
@@ -202,7 +202,7 @@
         tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
                congs wfs name R eqs;
     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
-    val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simps.add,
+    val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Simps.add,
       Code.add_default_eqn_attribute, Quickcheck_RecFun_Simps.add] else [];
 
     val ((simps' :: rules', [induct']), thy) =
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Tools/record.ML	Thu Oct 22 09:50:29 2009 +0200
@@ -2323,8 +2323,7 @@
     val final_thy =
       thms_thy
       |> (snd oo PureThy.add_thmss)
-          [((Binding.name "simps", sel_upd_simps),
-            [Simplifier.simp_add, Nitpick_Const_Simps.add]),
+          [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
            ((Binding.name "iffs", iffs), [iff_add])]
       |> put_record name (make_record_info args parent fields extension induct_scheme' ext_def)
       |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs')
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/Tools/refute.ML	Thu Oct 22 09:50:29 2009 +0200
@@ -1145,6 +1145,10 @@
   fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver,
     expect} t negate =
   let
+    (* string -> unit *)
+    fun check_expect outcome_code =
+      if expect = "" orelse outcome_code = expect then ()
+      else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
     (* unit -> unit *)
     fun wrapper () =
     let
@@ -1237,8 +1241,7 @@
           "unknown")
         val outcome_code = find_model_loop (first_universe types sizes minsize)
       in
-        if expect = "" orelse outcome_code = expect then ()
-        else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
+        check_expect outcome_code
       end
     in
       (* some parameter sanity checks *)
@@ -1261,9 +1264,10 @@
         TimeLimit.timeLimit (Time.fromSeconds maxtime)
           wrapper ()
         handle TimeLimit.TimeOut =>
-          priority ("Search terminated, time limit (" ^
-            string_of_int maxtime
-            ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.")
+          (priority ("Search terminated, time limit (" ^
+              string_of_int maxtime
+              ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.");
+           check_expect "unknown")
       ) else
         wrapper ()
     end;
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/UNITY/Extend.thy
--- a/src/HOL/UNITY/Extend.thy	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/UNITY/Extend.thy	Thu Oct 22 09:50:29 2009 +0200
@@ -121,7 +121,7 @@
      assumes surj_h: "surj h"
          and prem:   "!! x y. g (h(x,y)) = x"
      shows "fst (inv h z) = g z"
-by (metis UNIV_I f_inv_onto_f pair_collapse prem surj_h surj_range)
+by (metis UNIV_I f_inv_into_f pair_collapse prem surj_h surj_range)
 
 
 subsection{*Trivial properties of f, g, h*}
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/ZF/HOLZF.thy
--- a/src/HOL/ZF/HOLZF.thy	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/ZF/HOLZF.thy	Thu Oct 22 09:50:29 2009 +0200
@@ -626,7 +626,7 @@
 
 lemma nat2Nat_Nat2nat[simp]: "Elem n Nat \<Longrightarrow> nat2Nat (Nat2nat n) = n"
   apply (simp add: Nat2nat_def)
-  apply (rule_tac f_inv_onto_f)
+  apply (rule_tac f_inv_into_f)
   apply (auto simp add: image_def Nat_def Sep)
   done
 
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/ZF/Zet.thy
--- a/src/HOL/ZF/Zet.thy	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/ZF/Zet.thy	Thu Oct 22 09:50:29 2009 +0200
@@ -35,7 +35,7 @@
 
 lemma image_zet_rep: "A \<in> zet \<Longrightarrow> ? z . g ` A = explode z"
   apply (auto simp add: zet_def')
-  apply (rule_tac x="Repl z (g o (inv_onto A f))" in exI)
+  apply (rule_tac x="Repl z (g o (inv_into A f))" in exI)
   apply (simp add: explode_Repl_eq)
   apply (subgoal_tac "explode z = f ` A")
   apply (simp_all add: comp_image_eq)
@@ -49,10 +49,10 @@
     by (auto simp add: zet_def')
   then obtain f where injf: "inj_on (f :: _ \<Rightarrow> ZF) A"  
     by auto
-  let ?w = "f o (inv_onto A g)"
-  have subset: "(inv_onto A g) ` (g ` A) \<subseteq> A"
-    by (auto simp add: inv_onto_into)
-  have "inj_on (inv_onto A g) (g ` A)" by (simp add: inj_on_inv_onto)
+  let ?w = "f o (inv_into A g)"
+  have subset: "(inv_into A g) ` (g ` A) \<subseteq> A"
+    by (auto simp add: inv_into_into)
+  have "inj_on (inv_into A g) (g ` A)" by (simp add: inj_on_inv_into)
   then have injw: "inj_on ?w (g ` A)"
     apply (rule comp_inj_on)
     apply (rule subset_inj_on[where B=A])
@@ -86,7 +86,7 @@
 lemma zexplode_zimplode: "zexplode (zimplode A) = A"
   apply (simp add: zimplode_def zexplode_def)
   apply (simp add: implode_def)
-  apply (subst f_inv_onto_f[where y="Rep_zet A"])
+  apply (subst f_inv_into_f[where y="Rep_zet A"])
   apply (auto simp add: Rep_zet_inverse Rep_zet_eq_explode image_def)
   done
 
diff -r 70f5c18e975d -r d1c9bf0f8ae8 src/HOL/ex/set.thy
--- a/src/HOL/ex/set.thy	Thu Oct 22 09:49:48 2009 +0200
+++ b/src/HOL/ex/set.thy	Thu Oct 22 09:50:29 2009 +0200
@@ -104,7 +104,7 @@
     --{*The term above can be synthesized by a sufficiently detailed proof.*}
   apply (rule bij_if_then_else)
      apply (rule_tac [4] refl)
-    apply (rule_tac [2] inj_on_inv_onto)
+    apply (rule_tac [2] inj_on_inv_into)
     apply (erule subset_inj_on [OF _ subset_UNIV])
    apply blast
   apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])