src/HOL/Quotient.thy
changeset 53011 aeee0a4be6cf
parent 51112 da97167e03f7
child 54555 e8c5e95d338b
     1.1 --- a/src/HOL/Quotient.thy	Tue Aug 13 15:59:22 2013 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Tue Aug 13 15:59:22 2013 +0200
     1.3 @@ -28,6 +28,10 @@
     1.4    shows "((op =) OOO R) = R"
     1.5    by (auto simp add: fun_eq_iff)
     1.6  
     1.7 +context
     1.8 +begin
     1.9 +interpretation lifting_syntax .
    1.10 +
    1.11  subsection {* Quotient Predicate *}
    1.12  
    1.13  definition
    1.14 @@ -578,6 +582,7 @@
    1.15    shows "(Rep ---> Abs) id = id"
    1.16    by (simp add: fun_eq_iff Quotient3_abs_rep [OF a])
    1.17  
    1.18 +end
    1.19  
    1.20  locale quot_type =
    1.21    fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.22 @@ -812,10 +817,15 @@
    1.23  lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
    1.24    by (simp add: Quot_True_def)
    1.25  
    1.26 +context 
    1.27 +begin
    1.28 +interpretation lifting_syntax .
    1.29  
    1.30  text {* Tactics for proving the lifted theorems *}
    1.31  ML_file "Tools/Quotient/quotient_tacs.ML"
    1.32  
    1.33 +end
    1.34 +
    1.35  subsection {* Methods / Interface *}
    1.36  
    1.37  method_setup lifting =
    1.38 @@ -862,9 +872,7 @@
    1.39    {* lift theorems to quotient types *}
    1.40  
    1.41  no_notation
    1.42 -  rel_conj (infixr "OOO" 75) and
    1.43 -  map_fun (infixr "--->" 55) and
    1.44 -  fun_rel (infixr "===>" 55)
    1.45 +  rel_conj (infixr "OOO" 75)
    1.46  
    1.47  end
    1.48