# HG changeset patch
# User kuncar
# Date 1376402362 -7200
# Node ID aeee0a4be6cfad98f1790b2a02e5a588e4c7c978
# Parent  ec5e6f69bd653a31f222771c5b574832bbb75a56
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local

diff -r ec5e6f69bd65 -r aeee0a4be6cf src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Tue Aug 13 15:59:22 2013 +0200
+++ b/src/HOL/Lifting.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -16,7 +16,9 @@
 
 subsection {* Function map *}
 
-notation map_fun (infixr "--->" 55)
+context
+begin
+interpretation lifting_syntax .
 
 lemma map_fun_id:
   "(id ---> id) = id"
@@ -599,6 +601,8 @@
   shows "Domainp T = P"
 by (simp add: invariant_def Domainp_iff[abs_def] Quotient_cr_rel[OF assms])
 
+end
+
 subsection {* ML setup *}
 
 ML_file "Tools/Lifting/lifting_util.ML"
diff -r ec5e6f69bd65 -r aeee0a4be6cf src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Tue Aug 13 15:59:22 2013 +0200
+++ b/src/HOL/Quotient.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -28,6 +28,10 @@
   shows "((op =) OOO R) = R"
   by (auto simp add: fun_eq_iff)
 
+context
+begin
+interpretation lifting_syntax .
+
 subsection {* Quotient Predicate *}
 
 definition
@@ -578,6 +582,7 @@
   shows "(Rep ---> Abs) id = id"
   by (simp add: fun_eq_iff Quotient3_abs_rep [OF a])
 
+end
 
 locale quot_type =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
@@ -812,10 +817,15 @@
 lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
   by (simp add: Quot_True_def)
 
+context 
+begin
+interpretation lifting_syntax .
 
 text {* Tactics for proving the lifted theorems *}
 ML_file "Tools/Quotient/quotient_tacs.ML"
 
+end
+
 subsection {* Methods / Interface *}
 
 method_setup lifting =
@@ -862,9 +872,7 @@
   {* lift theorems to quotient types *}
 
 no_notation
-  rel_conj (infixr "OOO" 75) and
-  map_fun (infixr "--->" 55) and
-  fun_rel (infixr "===>" 55)
+  rel_conj (infixr "OOO" 75)
 
 end
 
diff -r ec5e6f69bd65 -r aeee0a4be6cf src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Tue Aug 13 15:59:22 2013 +0200
+++ b/src/HOL/Transfer.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -12,10 +12,20 @@
 subsection {* Relator for function space *}
 
 definition
-  fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool" (infixr "===>" 55)
+  fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
 where
   "fun_rel A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
 
+locale lifting_syntax
+begin
+  notation fun_rel (infixr "===>" 55)
+  notation map_fun (infixr "--->" 55)
+end
+
+context
+begin
+interpretation lifting_syntax .
+
 lemma fun_relI [intro]:
   assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
   shows "(A ===> B) f g"
@@ -112,6 +122,8 @@
   shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
   using assms unfolding Rel_def fun_rel_def by fast
 
+end
+
 ML_file "Tools/transfer.ML"
 setup Transfer.setup
 
@@ -121,6 +133,10 @@
 
 hide_const (open) Rel
 
+context
+begin
+interpretation lifting_syntax .
+
 text {* Handling of domains *}
 
 lemma Domaimp_refl[transfer_domain_rule]:
@@ -358,3 +374,5 @@
   unfolding transfer_forall_def by (rule All_transfer)
 
 end
+
+end