src/HOL/Product_Type.thy
changeset 14565 c6dc17aab88a
parent 14359 3d9948163018
child 14952 47455995693d
     1.1 --- a/src/HOL/Product_Type.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -159,6 +159,10 @@
     1.4    "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
     1.5    "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
     1.6  
     1.7 +syntax (HTML output)
     1.8 +  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
     1.9 +  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
    1.10 +
    1.11  print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
    1.12  
    1.13