src/HOL/Lattice/Orders.thy

   The classes of quasi and partial orders are closed under binary
   products.  Note that the direct product of linear orders need
   \emph{not} be linear in general.
 *}
 
-instantiation * :: (leq, leq) leq
+instantiation prod :: (leq, leq) leq
 begin
 
 definition
   leq_prod_def: "p \<sqsubseteq> q \<equiv> fst p \<sqsubseteq> fst q \<and> snd p \<sqsubseteq> snd q"
 

 
 lemma leq_prodE [elim?]:
     "p \<sqsubseteq> q \<Longrightarrow> (fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> C) \<Longrightarrow> C"
   by (unfold leq_prod_def) blast
 
-instance * :: (quasi_order, quasi_order) quasi_order
+instance prod :: (quasi_order, quasi_order) quasi_order
 proof
   fix p q r :: "'a::quasi_order \<times> 'b::quasi_order"
   show "p \<sqsubseteq> p"
   proof
     show "fst p \<sqsubseteq> fst p" ..

     also from qr have "\<dots> \<sqsubseteq> snd r" ..
     finally show "snd p \<sqsubseteq> snd r" .
   qed
 qed
 
-instance * :: (partial_order, partial_order) partial_order
+instance prod :: (partial_order, partial_order) partial_order
 proof
   fix p q :: "'a::partial_order \<times> 'b::partial_order"
   assume pq: "p \<sqsubseteq> q" and qp: "q \<sqsubseteq> p"
   show "p = q"
   proof