src/HOL/Transfer.thy
changeset 63343 fb5d8a50c641
parent 63092 a949b2a5f51d
child 64014 ca1239a3277b
     1.1 --- a/src/HOL/Transfer.thy	Tue Jun 21 17:35:45 2016 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Wed Jun 22 10:09:20 2016 +0200
     1.3 @@ -11,15 +11,14 @@
     1.4  
     1.5  subsection \<open>Relator for function space\<close>
     1.6  
     1.7 -locale lifting_syntax
     1.8 +bundle lifting_syntax
     1.9  begin
    1.10 -  notation rel_fun (infixr "===>" 55)
    1.11 -  notation map_fun (infixr "--->" 55)
    1.12 +  notation rel_fun  (infixr "===>" 55)
    1.13 +  notation map_fun  (infixr "--->" 55)
    1.14  end
    1.15  
    1.16 -context
    1.17 +context includes lifting_syntax
    1.18  begin
    1.19 -interpretation lifting_syntax .
    1.20  
    1.21  lemma rel_funD2:
    1.22    assumes "rel_fun A B f g" and "A x x"
    1.23 @@ -236,9 +235,8 @@
    1.24  
    1.25  hide_const (open) Rel
    1.26  
    1.27 -context
    1.28 +context includes lifting_syntax
    1.29  begin
    1.30 -interpretation lifting_syntax .
    1.31  
    1.32  text \<open>Handling of domains\<close>
    1.33  
    1.34 @@ -365,9 +363,8 @@
    1.35  
    1.36  subsection \<open>Transfer rules\<close>
    1.37  
    1.38 -context
    1.39 +context includes lifting_syntax
    1.40  begin
    1.41 -interpretation lifting_syntax .
    1.42  
    1.43  lemma Domainp_forall_transfer [transfer_rule]:
    1.44    assumes "right_total A"