changeset 65366 | 10ca63a18e56 |
parent 63649 | e690d6f2185b |
child 66244 | 4c999b5d78e2 |
--- 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 \<open>Formalisation of chain-complete partial orders, continuity and admissibility\<close> theory Complete_Partial_Order2 imports - Main - "~~/src/HOL/Library/Lattice_Syntax" + Main Lattice_Syntax begin lemma chain_transfer [transfer_rule]: