src/HOL/Library/Product_ord.thy
changeset 37678 0040bafffdef
parent 31040 996ae76c9eda
child 37765 26bdfb7b680b
     1.1 --- a/src/HOL/Library/Product_ord.thy	Thu Jul 01 16:54:42 2010 +0200
     1.2 +++ b/src/HOL/Library/Product_ord.thy	Thu Jul 01 16:54:44 2010 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -instantiation "*" :: (ord, ord) ord
     1.8 +instantiation prod :: (ord, ord) ord
     1.9  begin
    1.10  
    1.11  definition
    1.12 @@ -26,16 +26,16 @@
    1.13    "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
    1.14    unfolding prod_le_def prod_less_def by simp_all
    1.15  
    1.16 -instance * :: (preorder, preorder) preorder proof
    1.17 +instance prod :: (preorder, preorder) preorder proof
    1.18  qed (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans)
    1.19  
    1.20 -instance * :: (order, order) order proof
    1.21 +instance prod :: (order, order) order proof
    1.22  qed (auto simp add: prod_le_def)
    1.23  
    1.24 -instance * :: (linorder, linorder) linorder proof
    1.25 +instance prod :: (linorder, linorder) linorder proof
    1.26  qed (auto simp: prod_le_def)
    1.27  
    1.28 -instantiation * :: (linorder, linorder) distrib_lattice
    1.29 +instantiation prod :: (linorder, linorder) distrib_lattice
    1.30  begin
    1.31  
    1.32  definition
    1.33 @@ -49,7 +49,7 @@
    1.34  
    1.35  end
    1.36  
    1.37 -instantiation * :: (bot, bot) bot
    1.38 +instantiation prod :: (bot, bot) bot
    1.39  begin
    1.40  
    1.41  definition
    1.42 @@ -60,7 +60,7 @@
    1.43  
    1.44  end
    1.45  
    1.46 -instantiation * :: (top, top) top
    1.47 +instantiation prod :: (top, top) top
    1.48  begin
    1.49  
    1.50  definition