src/Doc/Main/Main_Doc.thy
changeset 69313 b021008c5397
parent 69108 e2780bb26395
child 69597 ff784d5a5bfb
     1.1 --- a/src/Doc/Main/Main_Doc.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/Doc/Main/Main_Doc.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -112,8 +112,6 @@
     1.4  @{const Set.member} & @{term_type_only Set.member "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\<^verbatim>\<open>:\<close>)\\
     1.5  @{const Set.union} & @{term_type_only Set.union "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\<^verbatim>\<open>Un\<close>)\\
     1.6  @{const Set.inter} & @{term_type_only Set.inter "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\<^verbatim>\<open>Int\<close>)\\
     1.7 -@{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
     1.8 -@{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
     1.9  @{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\
    1.10  @{const Inter} & @{term_type_only Inter "'a set set\<Rightarrow>'a set"}\\
    1.11  @{const Pow} & @{term_type_only Pow "'a set \<Rightarrow>'a set set"}\\
    1.12 @@ -134,10 +132,10 @@
    1.13  @{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\
    1.14  @{term "{x. P}"} & @{term[source]"Collect (\<lambda>x. P)"}\\
    1.15  \<open>{t | x\<^sub>1 \<dots> x\<^sub>n. P}\<close> & \<open>{v. \<exists>x\<^sub>1 \<dots> x\<^sub>n. v = t \<and> P}\<close>\\
    1.16 -@{term[source]"\<Union>x\<in>I. A"} & @{term[source]"UNION I (\<lambda>x. A)"} & (\texttt{UN})\\
    1.17 -@{term[source]"\<Union>x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\
    1.18 -@{term[source]"\<Inter>x\<in>I. A"} & @{term[source]"INTER I (\<lambda>x. A)"} & (\texttt{INT})\\
    1.19 -@{term[source]"\<Inter>x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\
    1.20 +@{term[source]"\<Union>x\<in>I. A"} & @{term[source]"\<Union>((\<lambda>x. A) ` I)"} & (\texttt{UN})\\
    1.21 +@{term[source]"\<Union>x. A"} & @{term[source]"\<Union>((\<lambda>x. A) ` UNIV)"}\\
    1.22 +@{term[source]"\<Inter>x\<in>I. A"} & @{term[source]"\<Inter>((\<lambda>x. A) ` I)"} & (\texttt{INT})\\
    1.23 +@{term[source]"\<Inter>x. A"} & @{term[source]"\<Inter>((\<lambda>x. A) ` UNIV)"}\\
    1.24  @{term "\<forall>x\<in>A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\
    1.25  @{term "\<exists>x\<in>A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\
    1.26  @{term "range f"} & @{term[source]"f ` UNIV"}\\