src/HOL/Lifting.thy
changeset 53011 aeee0a4be6cf
parent 52307 32c433c38ddd
child 53151 fbf4d50dec91
     1.1 --- a/src/HOL/Lifting.thy	Tue Aug 13 15:59:22 2013 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Tue Aug 13 15:59:22 2013 +0200
     1.3 @@ -16,7 +16,9 @@
     1.4  
     1.5  subsection {* Function map *}
     1.6  
     1.7 -notation map_fun (infixr "--->" 55)
     1.8 +context
     1.9 +begin
    1.10 +interpretation lifting_syntax .
    1.11  
    1.12  lemma map_fun_id:
    1.13    "(id ---> id) = id"
    1.14 @@ -599,6 +601,8 @@
    1.15    shows "Domainp T = P"
    1.16  by (simp add: invariant_def Domainp_iff[abs_def] Quotient_cr_rel[OF assms])
    1.17  
    1.18 +end
    1.19 +
    1.20  subsection {* ML setup *}
    1.21  
    1.22  ML_file "Tools/Lifting/lifting_util.ML"