(* defined in Orders.thy *) val leq_refl = thm "leq_refl" ; val leq_trans = thm "leq_trans" ; val leq_antisym = thm "leq_antisym" ; val leq_linear = thm "leq_linear" ; val [set_leq_refl, set_leq_trans, set_leq_antisym] = map (fold_rule [set_leq_def] o transfer Lat1.thy) [subset_refl, subset_trans, subset_antisym] ; (* defined in Bounds.thy *) val is_inf_def = thm "is_inf_def" ; val is_Inf_def = thm "is_Inf_def" ; val is_sup_def = thm "is_sup_def" ; val is_Sup_def = thm "is_Sup_def" ; (* defined in Lattice.thy *) val ex_inf = thm "ex_inf" ; val ex_sup = thm "ex_sup" ; (* defined in CompleteLattice.thy *) val top_def = thm "top_def" ; val bottom_def = thm "bottom_def" ; val bottom_least = thm "bottom_least" ; val top_greatest = thm "top_greatest" ;