1.1 --- a/src/HOL/Docs/MainDoc.thy	Sun Mar 08 21:35:39 2009 +0100
     1.2 +++ b/src/HOL/Docs/MainDoc.thy	Mon Mar 09 09:24:50 2009 +0100
     1.3 @@ -74,23 +74,22 @@
     1.4  @{term"ALL x<y. P"} & @{term[source]"\<forall>x. x < y \<longrightarrow> P"}\\
     1.5  @{term"ALL x>=y. P"} & @{term[source]"\<forall>x. x \<ge> y \<longrightarrow> P"}\\
     1.6  @{term"ALL x>y. P"} & @{term[source]"\<forall>x. x > y \<longrightarrow> P"}\\
     1.7 +\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<exists>"} instead of @{text"\<forall>"}}\\
     1.8  @{term"LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\
     1.9  \end{supertabular}
    1.10  
    1.11 -Similar for @{text"\<exists>"} instead of @{text"\<forall>"}.
    1.12 -
    1.13  \section{Set}
    1.14  
    1.15  Sets are predicates: @{text[source]"'a set  =  'a \<Rightarrow> bool"}
    1.16  \bigskip
    1.17  
    1.18  \begin{supertabular}{@ {} l @ {~::~} l @ {}}
    1.19 -@{const "{}"} & @{term_type_only "{}" "'a set"}\\
    1.20 +@{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\
    1.21  @{const insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\
    1.22  @{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\
    1.23 -@{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"}\\
    1.24 -@{const "op Un"} & @{term_type_only "op Un" "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"}\\
    1.25 -@{const "op Int"} & @{term_type_only "op Int" "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"}\\
    1.26 +@{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"} \qquad(\textsc{ascii} @{text":"})\\
    1.27 +@{const Set.Un} & @{term_type_only Set.Un "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} \qquad(\textsc{ascii} @{text"Un"})\\
    1.28 +@{const Set.Int} & @{term_type_only Set.Int "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} \qquad(\textsc{ascii} @{text"Int"})\\
    1.29  @{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
    1.30  @{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
    1.31  @{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\
    1.32 @@ -112,10 +111,10 @@
    1.33  @{term[source]"A \<supseteq> B"} & @{term[source]"B \<le> A"}\\
    1.34  @{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\
    1.35  @{term"{x. P}"} & @{term[source]"Collect(\<lambda>x. P)"}\\
    1.36 -@{term"UN x:I. A"} & @{term[source]"UNION I (\<lambda>x. A)"}\\
    1.37 -@{term"UN x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\
    1.38 -@{term"INT x:I. A"} & @{term[source]"INTER I (\<lambda>x. A)"}\\
    1.39 -@{term"INT x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\
    1.40 +@{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\<lambda>x. A)"}\\
    1.41 +@{term[mode=xsymbols]"UN x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\
    1.42 +@{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\<lambda>x. A)"}\\
    1.43 +@{term[mode=xsymbols]"INT x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\
    1.44  @{term"ALL x:A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\
    1.45  @{term"EX x:A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\
    1.46  @{term"range f"} & @{term[source]"f ` UNIV"}\\
    1.47 @@ -345,14 +344,14 @@
    1.48  \section{Set\_Interval}
    1.49  
    1.50  \begin{supertabular}{@ {} l @ {~::~} l @ {}}
    1.51 -@{const lessThan} & @{typeof lessThan}\\
    1.52 -@{const atMost} & @{typeof atMost}\\
    1.53 -@{const greaterThan} & @{typeof greaterThan}\\
    1.54 -@{const atLeast} & @{typeof atLeast}\\
    1.55 -@{const greaterThanLessThan} & @{typeof greaterThanLessThan}\\
    1.56 -@{const atLeastLessThan} & @{typeof atLeastLessThan}\\
    1.57 -@{const greaterThanAtMost} & @{typeof greaterThanAtMost}\\
    1.58 -@{const atLeastAtMost} & @{typeof atLeastAtMost}\\
    1.59 +@{const lessThan} & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\
    1.60 +@{const atMost} & @{term_type_only atMost "'a::ord \<Rightarrow> 'a set"}\\
    1.61 +@{const greaterThan} & @{term_type_only greaterThan "'a::ord \<Rightarrow> 'a set"}\\
    1.62 +@{const atLeast} & @{term_type_only atLeast "'a::ord \<Rightarrow> 'a set"}\\
    1.63 +@{const greaterThanLessThan} & @{term_type_only greaterThanLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
    1.64 +@{const atLeastLessThan} & @{term_type_only atLeastLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
    1.65 +@{const greaterThanAtMost} & @{term_type_only greaterThanAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
    1.66 +@{const atLeastAtMost} & @{term_type_only atLeastAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
    1.67  \end{supertabular}
    1.68  
    1.69  \subsubsection*{Syntax}
    1.70 @@ -366,8 +365,11 @@
    1.71  @{term "atLeastLessThan x y"} & @{term[source] "atLeastLessThan x y"}\\
    1.72  @{term "greaterThanAtMost x y"} & @{term[source] "greaterThanAtMost x y"}\\
    1.73  @{term "atLeastAtMost x y"} & @{term[source] "atLeastAtMost x y"}\\
    1.74 -@{term "UN i:{..n}. A"} & @{term[source] "\<Union> i \<in> {..n}. A"}\\
    1.75 +@{term[mode=xsymbols] "UN i:{..n}. A"} & @{term[source] "\<Union> i \<in> {..n}. A"}\\
    1.76 +@{term[mode=xsymbols] "UN i:{..<n}. A"} & @{term[source] "\<Union> i \<in> {..<n}. A"}\\
    1.77 +\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Inter>"} instead of @{text"\<Union>"}}\\
    1.78  @{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\
    1.79 +@{term "setsum (%x. t) {a..<b}"} & @{term[source] "setsum (\<lambda>x. t) {a..<b}"}\\
    1.80  \end{supertabular}
    1.81  
    1.82  ???????