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