--- a/src/HOL/Library/Complete_Partial_Order2.thy Mon Sep 20 23:15:02 2021 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Tue Sep 21 00:20:47 2021 +0200
@@ -5,9 +5,11 @@
section \<open>Formalisation of chain-complete partial orders, continuity and admissibility\<close>
theory Complete_Partial_Order2 imports
- Main Lattice_Syntax
+ Main
begin
+unbundle lattice_syntax
+
lemma chain_transfer [transfer_rule]:
includes lifting_syntax
shows "((A ===> A ===> (=)) ===> rel_set A ===> (=)) Complete_Partial_Order.chain Complete_Partial_Order.chain"