src/HOL/Prod.thy
changeset 6340 7d5cbd5819a0
parent 4875 cb48549230ce
child 8703 816d8f6513be
     1.1 --- a/src/HOL/Prod.thy	Wed Mar 10 10:53:53 1999 +0100
     1.2 +++ b/src/HOL/Prod.thy	Wed Mar 10 10:55:12 1999 +0100
     1.3 @@ -27,6 +27,9 @@
     1.4  syntax (symbols)
     1.5    "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
     1.6  
     1.7 +syntax (HTML output)
     1.8 +  "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
     1.9 +
    1.10  
    1.11  (* abstract constants and syntax *)
    1.12