diff -r d32e702d7ab8 -r 10ca63a18e56 src/HOL/Library/Complete_Partial_Order2.thy --- a/src/HOL/Library/Complete_Partial_Order2.thy Mon Apr 03 23:31:31 2017 +0200 +++ b/src/HOL/Library/Complete_Partial_Order2.thy Tue Apr 04 11:52:28 2017 +0200 @@ -5,8 +5,7 @@ section \Formalisation of chain-complete partial orders, continuity and admissibility\ theory Complete_Partial_Order2 imports - Main - "~~/src/HOL/Library/Lattice_Syntax" + Main Lattice_Syntax begin lemma chain_transfer [transfer_rule]: