| changeset 61585 | a9599d3d7610 |
| parent 60500 | 903bb1495239 |
| child 61969 | e01015e49041 |
--- a/src/HOL/Library/Lub_Glb.thy Thu Nov 05 10:35:37 2015 +0100 +++ b/src/HOL/Library/Lub_Glb.thy Thu Nov 05 10:39:49 2015 +0100 @@ -17,7 +17,7 @@ where "x <=* S = (ALL y: S. x \<le> y)" -subsection \<open>Rules for the Relations @{text "*<="} and @{text "<=*"}\<close> +subsection \<open>Rules for the Relations \<open>*<=\<close> and \<open><=*\<close>\<close> lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x" by (simp add: setle_def)