105 Sets are predicates: @{text[source]"'a set = 'a \<Rightarrow> bool"} |
105 Sets are predicates: @{text[source]"'a set = 'a \<Rightarrow> bool"} |
106 \bigskip |
106 \bigskip |
107 |
107 |
108 \begin{supertabular}{@ {} l @ {~::~} l l @ {}} |
108 \begin{supertabular}{@ {} l @ {~::~} l l @ {}} |
109 @{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\ |
109 @{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\ |
110 @{const insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\ |
110 @{const Set.insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\ |
111 @{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\ |
111 @{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\ |
112 @{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\texttt{:})\\ |
112 @{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\texttt{:})\\ |
113 @{const Set.Un} & @{term_type_only Set.Un "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Un})\\ |
113 @{const Set.union} & @{term_type_only Set.Un "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Un})\\ |
114 @{const Set.Int} & @{term_type_only Set.Int "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Int})\\ |
114 @{const Set.inter} & @{term_type_only Set.Int "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Int})\\ |
115 @{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\ |
115 @{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\ |
116 @{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\ |
116 @{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\ |
117 @{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\ |
117 @{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\ |
118 @{const Inter} & @{term_type_only Inter "'a set set\<Rightarrow>'a set"}\\ |
118 @{const Inter} & @{term_type_only Inter "'a set set\<Rightarrow>'a set"}\\ |
119 @{const Pow} & @{term_type_only Pow "'a set \<Rightarrow>'a set set"}\\ |
119 @{const Pow} & @{term_type_only Pow "'a set \<Rightarrow>'a set set"}\\ |