equal
deleted
inserted
replaced
154 in [("split", split_tr')] |
154 in [("split", split_tr')] |
155 end |
155 end |
156 *} |
156 *} |
157 |
157 |
158 syntax (xsymbols) |
158 syntax (xsymbols) |
|
159 "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\<Sigma> _\<in>_./ _)" 10) |
|
160 "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80) |
|
161 |
|
162 syntax (HTML output) |
159 "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\<Sigma> _\<in>_./ _)" 10) |
163 "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\<Sigma> _\<in>_./ _)" 10) |
160 "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80) |
164 "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80) |
161 |
165 |
162 print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *} |
166 print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *} |
163 |
167 |