# HG changeset patch
# User wenzelm
# Date 855758551 -3600
# Node ID 27cdd600a3b13c6c2a7fca6420beb127bdadf26a
# Parent  1effe74134860bb9ac15a7bcdf9161c9aa56274e
tuned names: partial order, linear order;

diff -r 1effe7413486 -r 27cdd600a3b1 src/HOL/AxClasses/Lattice/CLattice.thy
--- a/src/HOL/AxClasses/Lattice/CLattice.thy	Mon Feb 10 16:16:55 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/CLattice.thy	Wed Feb 12 15:42:31 1997 +0100
@@ -12,7 +12,7 @@
 CLattice = Order +
 
 axclass
-  clattice < order
+  clattice < partial_order
   ex_Inf       "ALL A. EX inf. is_Inf A inf"
   ex_Sup       "ALL A. EX sup. is_Sup A sup"
 
diff -r 1effe7413486 -r 27cdd600a3b1 src/HOL/AxClasses/Lattice/LatInsts.thy
--- a/src/HOL/AxClasses/Lattice/LatInsts.thy	Mon Feb 10 16:16:55 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/LatInsts.thy	Wed Feb 12 15:42:31 1997 +0100
@@ -11,7 +11,7 @@
 (* linear orders are lattices *)
 
 instance
-  lin_order < lattice                   (allI, exI, min_is_inf, max_is_sup)
+  linear_order < lattice                (allI, exI, min_is_inf, max_is_sup)
 
 
 (* complete lattices are lattices *)
@@ -36,6 +36,6 @@
 
 (*FIXME bug workaround (see also OrdInsts.thy)*)
 instance
-  dual :: (lin_order) lin_order         (le_dual_lin)
+  dual :: (linear_order) linear_order   (le_dual_linear)
 
 end
diff -r 1effe7413486 -r 27cdd600a3b1 src/HOL/AxClasses/Lattice/Lattice.thy
--- a/src/HOL/AxClasses/Lattice/Lattice.thy	Mon Feb 10 16:16:55 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/Lattice.thy	Wed Feb 12 15:42:31 1997 +0100
@@ -8,7 +8,7 @@
 Lattice = Order +
 
 axclass
-  lattice < order
+  lattice < partial_order
   ex_inf       "ALL x y. EX inf. is_inf x y inf"
   ex_sup       "ALL x y. EX sup. is_sup x y sup"
 
diff -r 1effe7413486 -r 27cdd600a3b1 src/HOL/AxClasses/Lattice/OrdDefs.ML
--- a/src/HOL/AxClasses/Lattice/OrdDefs.ML	Mon Feb 10 16:16:55 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML	Wed Feb 12 15:42:31 1997 +0100
@@ -20,7 +20,7 @@
   ba 1;
 qed "le_prod_trans";
 
-goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::order*'b::order)";
+goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::partial_order*'b::partial_order)";
   by (safe_tac (!claset));
   by (stac Pair_fst_snd_eq 1);
   br conjI 1;
@@ -44,7 +44,7 @@
   by (Fast_tac 1);
 qed "le_fun_trans";
 
-goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::order)";
+goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::partial_order)";
   by (safe_tac (!claset));
   br ext 1;
   br (le_antisym RS mp) 1;
@@ -72,7 +72,7 @@
   br le_trans 1;
 qed "le_dual_trans";
 
-goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::order dual)";
+goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)";
   by (safe_tac (!claset));
   br (Rep_dual_inverse RS subst) 1;
   br sym 1;
@@ -83,6 +83,6 @@
   ba 1;
 qed "le_dual_antisym";
 
-goalw thy [le_dual_def] "x [= y | y [= (x::'a::lin_order dual)";
-  br le_lin 1;
-qed "le_dual_lin";
+goalw thy [le_dual_def] "x [= y | y [= (x::'a::linear_order dual)";
+  br le_linear 1;
+qed "le_dual_linear";
diff -r 1effe7413486 -r 27cdd600a3b1 src/HOL/AxClasses/Lattice/OrdInsts.thy
--- a/src/HOL/AxClasses/Lattice/OrdInsts.thy	Mon Feb 10 16:16:55 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/OrdInsts.thy	Wed Feb 12 15:42:31 1997 +0100
@@ -14,30 +14,30 @@
   "*" :: (quasi_order, quasi_order) quasi_order         (le_prod_refl, le_prod_trans)
 
 instance
-  "*" :: (order, order) order                           (le_prod_antisym)
+  "*" :: (partial_order, partial_order) partial_order   (le_prod_antisym)
   
 
 instance
   fun :: (term, quasi_order) quasi_order                (le_fun_refl, le_fun_trans)
 
 instance
-  fun :: (term, order) order                            (le_fun_antisym)
+  fun :: (term, partial_order) partial_order            (le_fun_antisym)
 
 
-(* duals of quasi_orders / orders / lin_orders *)
+(* duals of quasi orders / partial orders / linear orders *)
 
 instance
   dual :: (quasi_order) quasi_order                     (le_dual_refl, le_dual_trans)
 
 instance
-  dual :: (order) order                                 (le_dual_antisym)
+  dual :: (partial_order) partial_order                 (le_dual_antisym)
 
 
 (*FIXME: had to be moved to LatInsts.thy due to some unpleasant
   'feature' in Pure/type.ML
 
 instance
-  dual :: (lin_order) lin_order                         (le_dual_lin)
+  dual :: (linear_order) linear_order                   (le_dual_lin)
 *)
 
 end
diff -r 1effe7413486 -r 27cdd600a3b1 src/HOL/AxClasses/Lattice/Order.ML
--- a/src/HOL/AxClasses/Lattice/Order.ML	Mon Feb 10 16:16:55 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/Order.ML	Wed Feb 12 15:42:31 1997 +0100
@@ -114,7 +114,7 @@
 
 (** limits in linear orders **)
 
-goalw thy [minimum_def, is_inf_def] "is_inf (x::'a::lin_order) y (minimum x y)";
+goalw thy [minimum_def, is_inf_def] "is_inf (x::'a::linear_order) y (minimum x y)";
   by (stac expand_if 1);
   by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   (*case "x [= y"*)
@@ -122,7 +122,7 @@
     ba 1;
     by (Fast_tac 1);
   (*case "~ x [= y"*)
-    br (le_lin RS disjE) 1;
+    br (le_linear RS disjE) 1;
     ba 1;
     be notE 1;
     ba 1;
@@ -130,7 +130,7 @@
     by (Fast_tac 1);
 qed "min_is_inf";
 
-goalw thy [maximum_def, is_sup_def] "is_sup (x::'a::lin_order) y (maximum x y)";
+goalw thy [maximum_def, is_sup_def] "is_sup (x::'a::linear_order) y (maximum x y)";
   by (stac expand_if 1);
   by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   (*case "x [= y"*)
@@ -139,7 +139,7 @@
     by (Fast_tac 1);
   (*case "~ x [= y"*)
     br le_refl 1;
-    br (le_lin RS disjE) 1;
+    br (le_linear RS disjE) 1;
     ba 1;
     be notE 1;
     ba 1;
diff -r 1effe7413486 -r 27cdd600a3b1 src/HOL/AxClasses/Lattice/Order.thy
--- a/src/HOL/AxClasses/Lattice/Order.thy	Mon Feb 10 16:16:55 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/Order.thy	Wed Feb 12 15:42:31 1997 +0100
@@ -31,15 +31,15 @@
 (* partial orders *)
 
 axclass
-  order < quasi_order
+  partial_order < quasi_order
   le_antisym    "x [= y & y [= x --> x = y"
 
 
 (* linear orders *)
 
 axclass
-  lin_order < order
-  le_lin        "x [= y | y [= x"
+  linear_order < partial_order
+  le_linear     "x [= y | y [= x"
 
 
 
@@ -49,11 +49,11 @@
 
 consts
   (*binary*)
-  is_inf        :: "['a::order, 'a, 'a] => bool"
-  is_sup        :: "['a::order, 'a, 'a] => bool"
+  is_inf        :: "['a::partial_order, 'a, 'a] => bool"
+  is_sup        :: "['a::partial_order, 'a, 'a] => bool"
   (*general*)
-  is_Inf        :: "['a::order set, 'a] => bool"
-  is_Sup        :: "['a::order set, 'a] => bool"
+  is_Inf        :: "['a::partial_order set, 'a] => bool"
+  is_Sup        :: "['a::partial_order set, 'a] => bool"
 
 defs
   is_inf_def    "is_inf x y inf ==
@@ -71,13 +71,13 @@
 
 
 
-(* binary minima and maxima (on lin_orders) *)
+(* binary minima and maxima (on linear_orders) *)
 
 constdefs
-  minimum      :: "['a::lin_order, 'a] => 'a"
+  minimum      :: "['a::linear_order, 'a] => 'a"
   "minimum x y == (if x [= y then x else y)"
 
-  maximum      :: "['a::lin_order, 'a] => 'a"
+  maximum      :: "['a::linear_order, 'a] => 'a"
   "maximum x y == (if x [= y then y else x)"
 
 end