equal
deleted
inserted
replaced
296 greater_eq (infix ">=" 50) where |
296 greater_eq (infix ">=" 50) where |
297 "x >= y \<equiv> y <= x" |
297 "x >= y \<equiv> y <= x" |
298 |
298 |
299 notation (input) |
299 notation (input) |
300 greater_eq (infix "\<ge>" 50) |
300 greater_eq (infix "\<ge>" 50) |
301 |
|
302 lemmas Least_def = Least_def [folded ord_class.Least] |
|
303 |
301 |
304 syntax |
302 syntax |
305 "_index1" :: index ("\<^sub>1") |
303 "_index1" :: index ("\<^sub>1") |
306 translations |
304 translations |
307 (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>" |
305 (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>" |