structure seql = struct val thy = theory "seql" end ; use_legacy_bindings seql.thy ; val _ = bind_thm ("meet_seq", transfer seql.thy seq_inf RS meet_equality) ; val _ = bind_thm ("join_seq", transfer seql.thy seq_sup RS join_equality) ;