| changeset 60586 | 1d31e3a50373 |
| parent 58880 | 0baae4311a9f |
| child 61260 | e6f03fae14d5 |
--- a/src/HOL/HOLCF/Porder.thy Fri Jun 26 10:20:33 2015 +0200 +++ b/src/HOL/HOLCF/Porder.thy Fri Jun 26 11:07:04 2015 +0200 @@ -126,7 +126,7 @@ "LUB n. t n == lub (range t)" notation (xsymbols) - Lub (binder "\<Squnion> " 10) + Lub (binder "\<Squnion>" 10) text {* access to some definition as inference rule *}