src/HOL/Library/Countable_Set_Type.thy
changeset 63343 fb5d8a50c641
parent 63040 eb4ddd18d635
child 66453 cc19f7ca2ed6
     1.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Tue Jun 21 17:35:45 2016 +0200
     1.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Wed Jun 22 10:09:20 2016 +0200
     1.3 @@ -70,8 +70,6 @@
     1.4  instantiation cset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
     1.5  begin
     1.6  
     1.7 -interpretation lifting_syntax .
     1.8 -
     1.9  lift_definition bot_cset :: "'a cset" is "{}" parametric empty_transfer by simp
    1.10  
    1.11  lift_definition less_eq_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> bool"
    1.12 @@ -81,6 +79,7 @@
    1.13  where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a cset)"
    1.14  
    1.15  lemma less_cset_transfer[transfer_rule]:
    1.16 +  includes lifting_syntax
    1.17    assumes [transfer_rule]: "bi_unique A"
    1.18    shows "((pcr_cset A) ===> (pcr_cset A) ===> op =) op \<subset> op <"
    1.19  unfolding less_cset_def[abs_def] psubset_eq[abs_def] by transfer_prover
    1.20 @@ -458,7 +457,8 @@
    1.21  
    1.22  text \<open>Unconditional transfer rules\<close>
    1.23  
    1.24 -context begin interpretation lifting_syntax .
    1.25 +context includes lifting_syntax
    1.26 +begin
    1.27  
    1.28  lemmas cempty_parametric [transfer_rule] = empty_transfer[Transfer.transferred]
    1.29