1.1 --- a/src/HOL/Lifting.thy	Mon Apr 16 23:23:08 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Mon Apr 16 20:50:43 2012 +0200
     1.3 @@ -256,7 +256,7 @@
     1.4  lemma typedef_to_Quotient:
     1.5    assumes "type_definition Rep Abs S"
     1.6    and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
     1.7 -  shows "Quotient (Lifting.invariant (\<lambda>x. x \<in> S)) Abs Rep T"
     1.8 +  shows "Quotient (invariant (\<lambda>x. x \<in> S)) Abs Rep T"
     1.9  proof -
    1.10    interpret type_definition Rep Abs S by fact
    1.11    from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
    1.12 @@ -265,14 +265,14 @@
    1.13  
    1.14  lemma typedef_to_part_equivp:
    1.15    assumes "type_definition Rep Abs S"
    1.16 -  shows "part_equivp (Lifting.invariant (\<lambda>x. x \<in> S))"
    1.17 +  shows "part_equivp (invariant (\<lambda>x. x \<in> S))"
    1.18  proof (intro part_equivpI)
    1.19    interpret type_definition Rep Abs S by fact
    1.20 -  show "\<exists>x. Lifting.invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def)
    1.21 +  show "\<exists>x. invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def)
    1.22  next
    1.23 -  show "symp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def)
    1.24 +  show "symp (invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def)
    1.25  next
    1.26 -  show "transp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def)
    1.27 +  show "transp (invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def)
    1.28  qed
    1.29  
    1.30  lemma open_typedef_to_Quotient: