--- a/src/HOL/Product_Type.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Product_Type.thy Wed Apr 14 14:13:05 2004 +0200
@@ -159,6 +159,10 @@
"@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\<Sigma> _\<in>_./ _)" 10)
"@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80)
+syntax (HTML output)
+ "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\<Sigma> _\<in>_./ _)" 10)
+ "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80)
+
print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}