src/HOL/Product_Type.thy
changeset 35427 ad039d29e01c
parent 35365 2fcd08c62495
child 35822 67e4de90d2c2
child 35828 46cfc4b8112e
equal deleted inserted replaced
35426:c9b9d4fc270d 35427:ad039d29e01c
   140 proof
   140 proof
   141   fix a b show "Pair_Rep a b \<in> ?Prod"
   141   fix a b show "Pair_Rep a b \<in> ?Prod"
   142     by rule+
   142     by rule+
   143 qed
   143 qed
   144 
   144 
   145 syntax (xsymbols)
   145 type_notation (xsymbols)
   146   "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
   146   "*"  ("(_ \<times>/ _)" [21, 20] 20)
   147 syntax (HTML output)
   147 type_notation (HTML output)
   148   "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
   148   "*"  ("(_ \<times>/ _)" [21, 20] 20)
   149 
   149 
   150 consts
   150 consts
   151   Pair     :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b"
   151   Pair     :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b"
   152   fst      :: "'a \<times> 'b \<Rightarrow> 'a"
   152   fst      :: "'a \<times> 'b \<Rightarrow> 'a"
   153   snd      :: "'a \<times> 'b \<Rightarrow> 'b"
   153   snd      :: "'a \<times> 'b \<Rightarrow> 'b"