src/HOL/Quotient.thy
changeset 63343 fb5d8a50c641
parent 61799 4cf66f21b764
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Quotient.thy	Tue Jun 21 17:35:45 2016 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Wed Jun 22 10:09:20 2016 +0200
     1.3 @@ -28,9 +28,8 @@
     1.4    shows "((op =) OOO R) = R"
     1.5    by (auto simp add: fun_eq_iff)
     1.6  
     1.7 -context
     1.8 +context includes lifting_syntax
     1.9  begin
    1.10 -interpretation lifting_syntax .
    1.11  
    1.12  subsection \<open>Quotient Predicate\<close>
    1.13  
    1.14 @@ -805,9 +804,8 @@
    1.15  lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
    1.16    by (simp add: Quot_True_def)
    1.17  
    1.18 -context 
    1.19 +context includes lifting_syntax
    1.20  begin
    1.21 -interpretation lifting_syntax .
    1.22  
    1.23  text \<open>Tactics for proving the lifted theorems\<close>
    1.24  ML_file "Tools/Quotient/quotient_tacs.ML"