# HG changeset patch # User nipkow # Date 1236587916 -3600 # Node ID 96d508968153b371ce8cbfe8cd9e0499fdd3df2a # Parent b3a60d828de0a67a7da9fcdbfdbeaaa26955bb3c UN syntax fix diff -r b3a60d828de0 -r 96d508968153 src/HOL/Docs/MainDoc.thy --- a/src/HOL/Docs/MainDoc.thy Mon Mar 09 09:24:50 2009 +0100 +++ b/src/HOL/Docs/MainDoc.thy Mon Mar 09 09:38:36 2009 +0100 @@ -370,6 +370,7 @@ \multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\"} instead of @{text"\"}}\\ @{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\x. t) {a..b}"}\\ @{term "setsum (%x. t) {a..x. t) {a.."} instead of @{text"\"}}\\ \end{supertabular} ??????? diff -r b3a60d828de0 -r 96d508968153 src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Mon Mar 09 09:24:50 2009 +0100 +++ b/src/HOL/SetInterval.thy Mon Mar 09 09:38:36 2009 +0100 @@ -59,13 +59,13 @@ "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3INT _<=_./ _)" 10) "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3INT _<_./ _)" 10) -syntax (input) +syntax (xsymbols) "@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3\ _\_./ _)" 10) "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3\ _<_./ _)" 10) "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3\ _\_./ _)" 10) "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\ _<_./ _)" 10) -syntax (xsymbols) +syntax (latex output) "@UNION_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00_ \ _)/ _)" 10) "@UNION_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00_ < _)/ _)" 10) "@INTER_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00_ \ _)/ _)" 10)