src/HOL/Library/Complete_Partial_Order2.thy
changeset 63343 fb5d8a50c641
parent 63243 1bc6816fd525
child 63649 e690d6f2185b
     1.1 --- a/src/HOL/Library/Complete_Partial_Order2.thy	Tue Jun 21 17:35:45 2016 +0200
     1.2 +++ b/src/HOL/Library/Complete_Partial_Order2.thy	Wed Jun 22 10:09:20 2016 +0200
     1.3 @@ -9,14 +9,11 @@
     1.4    "~~/src/HOL/Library/Lattice_Syntax"
     1.5  begin
     1.6  
     1.7 -context begin interpretation lifting_syntax .
     1.8 -
     1.9  lemma chain_transfer [transfer_rule]:
    1.10 -  "((A ===> A ===> op =) ===> rel_set A ===> op =) Complete_Partial_Order.chain Complete_Partial_Order.chain"
    1.11 +  includes lifting_syntax
    1.12 +  shows "((A ===> A ===> op =) ===> rel_set A ===> op =) Complete_Partial_Order.chain Complete_Partial_Order.chain"
    1.13  unfolding chain_def[abs_def] by transfer_prover
    1.14  
    1.15 -end
    1.16 -
    1.17  lemma linorder_chain [simp, intro!]:
    1.18    fixes Y :: "_ :: linorder set"
    1.19    shows "Complete_Partial_Order.chain op \<le> Y"