src/HOL/Transfer.thy
changeset 56543 9bd56f2e4c10
parent 56524 f4ba736040fa
child 56654 54326fa7afe6
     1.1 --- a/src/HOL/Transfer.thy	Fri Apr 11 22:53:47 2014 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Fri Apr 11 23:22:00 2014 +0200
     1.3 @@ -249,11 +249,6 @@
     1.4  setup Transfer.setup
     1.5  declare refl [transfer_rule]
     1.6  
     1.7 -ML_file "Tools/Transfer/transfer_bnf.ML" 
     1.8 -
     1.9 -declare pred_fun_def [simp]
    1.10 -declare rel_fun_eq [relator_eq]
    1.11 -
    1.12  hide_const (open) Rel
    1.13  
    1.14  context
    1.15 @@ -366,8 +361,19 @@
    1.16    unfolding bi_unique_alt_def bi_total_alt_def
    1.17    by (blast intro: right_unique_fun left_unique_fun)
    1.18  
    1.19 +end
    1.20 +
    1.21 +ML_file "Tools/Transfer/transfer_bnf.ML" 
    1.22 +
    1.23 +declare pred_fun_def [simp]
    1.24 +declare rel_fun_eq [relator_eq]
    1.25 +
    1.26  subsection {* Transfer rules *}
    1.27  
    1.28 +context
    1.29 +begin
    1.30 +interpretation lifting_syntax .
    1.31 +
    1.32  lemma Domainp_forall_transfer [transfer_rule]:
    1.33    assumes "right_total A"
    1.34    shows "((A ===> op =) ===> op =)