# HG changeset patch
# User kuncar
# Date 1334602243 -7200
# Node ID 0b9294e093dba47793b6c73e9e137d789848835d
# Parent  5024b37c489c1c6cb8ac6bfc43d140ab3781ede8
leave Lifting prefix

diff -r 5024b37c489c -r 0b9294e093db src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Mon Apr 16 23:23:08 2012 +0200
+++ b/src/HOL/Lifting.thy	Mon Apr 16 20:50:43 2012 +0200
@@ -256,7 +256,7 @@
 lemma typedef_to_Quotient:
   assumes "type_definition Rep Abs S"
   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
-  shows "Quotient (Lifting.invariant (\<lambda>x. x \<in> S)) Abs Rep T"
+  shows "Quotient (invariant (\<lambda>x. x \<in> S)) Abs Rep T"
 proof -
   interpret type_definition Rep Abs S by fact
   from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
@@ -265,14 +265,14 @@
 
 lemma typedef_to_part_equivp:
   assumes "type_definition Rep Abs S"
-  shows "part_equivp (Lifting.invariant (\<lambda>x. x \<in> S))"
+  shows "part_equivp (invariant (\<lambda>x. x \<in> S))"
 proof (intro part_equivpI)
   interpret type_definition Rep Abs S by fact
-  show "\<exists>x. Lifting.invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def)
+  show "\<exists>x. invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def)
 next
-  show "symp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def)
+  show "symp (invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def)
 next
-  show "transp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def)
+  show "transp (invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def)
 qed
 
 lemma open_typedef_to_Quotient: