# HG changeset patch
# User wenzelm
# Date 970590860 -7200
# Node ID c2a4dccf6e67232b35f580ec1fd0fad9fc28b6ff
# Parent  537206cc738f55d833fc946f5896f653f8feb2c1
reorganized AxClasses;

diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Group/Group.ML
--- a/src/HOL/AxClasses/Group/Group.ML	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,130 +0,0 @@
-(*  Title:      HOL/AxClasses/Group/Group.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Some basic theorems of group theory.
-*)
-
-fun sub r = standard (r RS subst);
-fun ssub r = standard (r RS ssubst);
-
-
-Goal "x * inverse x = (1::'a::group)";
-by (rtac (sub left_unit) 1);
-back();
-by (rtac (sub assoc) 1);
-by (rtac (sub left_inverse) 1);
-back();
-back();
-by (rtac (ssub assoc) 1);
-back();
-by (rtac (ssub left_inverse) 1);
-by (rtac (ssub assoc) 1);
-by (rtac (ssub left_unit) 1);
-by (rtac (ssub left_inverse) 1);
-by (rtac refl 1);
-qed "right_inverse";
-
-
-Goal "x * 1 = (x::'a::group)";
-by (rtac (sub left_inverse) 1);
-by (rtac (sub assoc) 1);
-by (rtac (ssub right_inverse) 1);
-by (rtac (ssub left_unit) 1);
-by (rtac refl 1);
-qed "right_unit";
-
-
-Goal "e * x = x --> e = (1::'a::group)";
-by (rtac impI 1);
-by (rtac (sub right_unit) 1);
-back();
-by (res_inst_tac [("x", "x")] (sub right_inverse) 1);
-by (rtac (sub assoc) 1);
-by (rtac arg_cong 1);
-back();
-by (assume_tac 1);
-qed "strong_one_unit";
-
-
-Goal "EX! e. ALL x. e * x = (x::'a::group)";
-by (rtac ex1I 1);
-by (rtac allI 1);
-by (rtac left_unit 1);
-by (rtac mp 1);
-by (rtac strong_one_unit 1);
-by (etac allE 1);
-by (assume_tac 1);
-qed "ex1_unit";
-
-
-Goal "ALL x. EX! e. e * x = (x::'a::group)";
-by (rtac allI 1);
-by (rtac ex1I 1);
-by (rtac left_unit 1);
-by (rtac (strong_one_unit RS mp) 1);
-by (assume_tac 1);
-qed "ex1_unit'";
-
-
-Goal "inj (op * (x::'a::group))";
-by (rtac injI 1);
-by (rtac (sub left_unit) 1);
-back();
-by (rtac (sub left_unit) 1);
-by (res_inst_tac [("x", "x")] (sub left_inverse) 1);
-by (rtac (ssub assoc) 1);
-back();
-by (rtac (ssub assoc) 1);
-by (rtac arg_cong 1);
-back();
-by (assume_tac 1);
-qed "inj_times";
-
-
-Goal "y * x = 1 --> y = inverse (x::'a::group)";
-by (rtac impI 1);
-by (rtac (sub right_unit) 1);
-back();
-back();
-by (rtac (sub right_unit) 1);
-by (res_inst_tac [("x", "x")] (sub right_inverse) 1);
-by (rtac (sub assoc) 1);
-by (rtac (sub assoc) 1);
-by (rtac arg_cong 1);
-back();
-by (rtac (ssub left_inverse) 1);
-by (assume_tac 1);
-qed "one_inverse";
-
-
-Goal "ALL x. EX! y. y * x = (1::'a::group)";
-by (rtac allI 1);
-by (rtac ex1I 1);
-by (rtac left_inverse 1);
-by (rtac mp 1);
-by (rtac one_inverse 1);
-by (assume_tac 1);
-qed "ex1_inverse";
-
-
-Goal "inverse (x * y) = inverse y * inverse (x::'a::group)";
-by (rtac sym 1);
-by (rtac mp 1);
-by (rtac one_inverse 1);
-by (rtac (ssub assoc) 1);
-by (rtac (sub assoc) 1);
-back();
-by (rtac (ssub left_inverse) 1);
-by (rtac (ssub left_unit) 1);
-by (rtac (ssub left_inverse) 1);
-by (rtac refl 1);
-qed "inverse_times";
-
-
-Goal "inverse (inverse x) = (x::'a::group)";
-by (rtac sym 1);
-by (rtac (one_inverse RS mp) 1);
-by (rtac (ssub right_inverse) 1);
-by (rtac refl 1);
-qed "inverse_inverse";
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Group/Group.thy
--- a/src/HOL/AxClasses/Group/Group.thy	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(*  Title:      Group.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-*)
-
-Group = Sigs + Fun +
-
-(* semigroups *)
-
-axclass
-  semigroup < times
-  assoc         "(x * y) * z = x * (y * z)"
-
-
-(* groups *)
-
-axclass
-  group < one, inverse, semigroup
-  left_unit     "1 * x = x"
-  left_inverse  "inverse x * x = 1"
-
-
-(* abelian groups *)
-
-axclass
-  agroup < group
-  commut        "x * y = y * x"
-
-end
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Group/GroupDefs.ML
--- a/src/HOL/AxClasses/Group/GroupDefs.ML	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-(* bool *)
-
-(*this is really overkill - should be rather proven 'inline'*)
-
-Goalw [times_bool_def] "(x * y) * z = x * (y * (z::bool))";
-by (Fast_tac 1);
-qed "bool_assoc";
-
-Goalw [times_bool_def, one_bool_def] "1 * x = (x::bool)";
-by (Fast_tac 1);
-qed "bool_left_unit";
-
-Goalw [times_bool_def, one_bool_def] "x * 1 = (x::bool)";
-by (Fast_tac 1);
-qed "bool_right_unit";
-
-Goalw [times_bool_def, inverse_bool_def, one_bool_def]
-  "inverse(x) * x = (1::bool)";
-by (Fast_tac 1);
-qed "bool_left_inverse";
-
-Goalw [times_bool_def] "x * y = (y * (x::bool))";
-by (Fast_tac 1);
-qed "bool_commut";
-
-
-(* cartesian products *)
-
-val prod_ss = simpset_of Prod.thy;
-
-Goalw [times_prod_def]
-  "(x * y) * z = x * (y * (z::'a::semigroup*'b::semigroup))";
-by (simp_tac (prod_ss addsimps [assoc]) 1);
-qed "prod_assoc";
-
-Goalw [times_prod_def, one_prod_def] "1 * x = (x::'a::monoid*'b::monoid)";
-by (simp_tac (prod_ss addsimps [Monoid.left_unit]) 1);
-qed "prod_left_unit";
-
-Goalw [times_prod_def, one_prod_def] "x * 1 = (x::'a::monoid*'b::monoid)";
-by (simp_tac (prod_ss addsimps [Monoid.right_unit]) 1);
-qed "prod_right_unit";
-
-Goalw [times_prod_def, inverse_prod_def, one_prod_def]
-  "inverse x * x = (1::'a::group*'b::group)";
-by (simp_tac (prod_ss addsimps [left_inverse]) 1);
-qed "prod_left_inverse";
-
-Goalw [times_prod_def] "x * y = y * (x::'a::agroup*'b::agroup)";
-by (simp_tac (prod_ss addsimps [commut]) 1);
-qed "prod_commut";
-
-
-(* function spaces *)
-
-Goalw [times_fun_def] "(x * y) * z = x * (y * (z::'a => 'b::semigroup))";
-by (stac expand_fun_eq 1);
-by (rtac allI 1);
-by (rtac assoc 1);
-qed "fun_assoc";
-
-Goalw [times_fun_def, one_fun_def] "1 * x = (x::'a => 'b::monoid)";
-by (stac expand_fun_eq 1);
-by (rtac allI 1);
-by (rtac Monoid.left_unit 1);
-qed "fun_left_unit";
-
-Goalw [times_fun_def, one_fun_def] "x * 1 = (x::'a => 'b::monoid)";
-by (stac expand_fun_eq 1);
-by (rtac allI 1);
-by (rtac Monoid.right_unit 1);
-qed "fun_right_unit";
-
-Goalw [times_fun_def, inverse_fun_def, one_fun_def]
-  "inverse x * x = (1::'a => 'b::group)";
-by (stac expand_fun_eq 1);
-by (rtac allI 1);
-by (rtac left_inverse 1);
-qed "fun_left_inverse";
-
-Goalw [times_fun_def] "x * y = y * (x::'a => 'b::agroup)";
-by (stac expand_fun_eq 1);
-by (rtac allI 1);
-by (rtac commut 1);
-qed "fun_commut";
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Group/GroupDefs.thy
--- a/src/HOL/AxClasses/Group/GroupDefs.thy	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(*  Title:      GroupDefs.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-*)
-
-GroupDefs = MonoidGroupInsts + Prod + Fun +
-
-
-(* bool *)
-
-instance
-  bool :: {times, inverse, one}
-
-defs
-  times_bool_def        "x * y == (x ~= y)"
-  inverse_bool_def      "inverse x == (x::bool)"
-  one_bool_def          "1 == False"
-
-
-(* cartesian products *)
-
-instance
-  "*" :: (term, term) {times, inverse, one}
-
-defs
-  times_prod_def        "p * q == (fst p * fst q, snd p * snd q)"
-  inverse_prod_def      "inverse p == (inverse (fst p), inverse (snd p))"
-  one_prod_def          "1 == (1, 1)"
-
-
-(* function spaces *)
-
-instance
-  fun :: (term, term) {times, inverse, one}
-
-defs
-  times_fun_def         "f * g == (%x. f x * g x)"
-  inverse_fun_def       "inverse f == (%x. inverse (f x))"
-  one_fun_def           "1 == (%x. 1)"
-
-end
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Group/GroupInsts.thy
--- a/src/HOL/AxClasses/Group/GroupInsts.thy	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(*  Title:      GroupInsts.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Some concrete instantiations: 'structures' and 'functors'.
-*)
-
-GroupInsts = GroupDefs +
-
-
-(* bool *)
-
-instance
-  bool :: semigroup              (bool_assoc)
-instance
-  bool :: monoid                 (bool_assoc, bool_left_unit, bool_right_unit)
-instance
-  bool :: group                  (bool_left_unit, bool_left_inverse)
-instance
-  bool :: agroup                 (bool_commut)
-
-
-(* cartesian products *)
-
-instance
-  "*" :: (semigroup, semigroup) semigroup   (prod_assoc)
-instance
-  "*" :: (monoid, monoid) monoid  (prod_assoc, prod_left_unit, prod_right_unit)
-instance
-  "*" :: (group, group) group               (prod_left_unit, prod_left_inverse)
-instance
-  "*" :: (agroup, agroup) agroup            (prod_commut)
-
-
-(* function spaces *)
-
-instance
-  fun :: (term, semigroup) semigroup        (fun_assoc)
-instance
-  fun :: (term, monoid) monoid       (fun_assoc, fun_left_unit, fun_right_unit)
-instance
-  fun :: (term, group) group                (fun_left_unit, fun_left_inverse)
-instance
-  fun :: (term, agroup) agroup              (fun_commut)
-
-end
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Group/Monoid.thy
--- a/src/HOL/AxClasses/Group/Monoid.thy	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  Title:      Monoid.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-*)
-
-Monoid = Sigs +
-
-(* monoids *)
-
-axclass
-  monoid < times, one
-  assoc         "(x * y) * z = x * (y * z)"
-  left_unit     "1 * x = x"
-  right_unit    "x * 1 = x"
-
-end
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Group/MonoidGroupInsts.thy
--- a/src/HOL/AxClasses/Group/MonoidGroupInsts.thy	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(*  Title:      MonoidGroupInsts.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Some class inclusions or 'abstract instantiations'.
-*)
-
-MonoidGroupInsts = Group + Monoid +
-
-
-(* monoids are semigroups *)
-
-instance
-  monoid < semigroup            (Monoid.assoc)
-
-
-(* groups are monoids *)
-
-instance
-  group < monoid                ("Group.assoc", "Group.left_unit", "Group.right_unit")
-
-end
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Group/ROOT.ML
--- a/src/HOL/AxClasses/Group/ROOT.ML	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(*  Title:      HOL/AxClasses/Group/ROOT.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Some bits of group theory via axiomatic type classes.
-*)
-
-set show_types;
-set show_sorts;
-
-time_use_thy "Monoid";
-time_use_thy "Group";
-time_use_thy "MonoidGroupInsts";
-time_use_thy "GroupInsts";
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Group/Sigs.thy
--- a/src/HOL/AxClasses/Group/Sigs.thy	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(*  Title:      Sigs.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-*)
-
-Sigs = HOL +
-
-axclass
-  inverse < term
-
-axclass
-  one < term
-
-consts
-  inverse :: 'a::inverse => 'a
-  "1"     :: 'a::one                    ("1")
-
-end
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Lattice/CLattice.ML
--- a/src/HOL/AxClasses/Lattice/CLattice.ML	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,180 +0,0 @@
-
-(** basic properties of "Inf" and "Sup" **)
-
-(* unique existence *)
-
-Goalw [Inf_def] "is_Inf A (Inf A)";
-  by (rtac (ex_Inf RS spec RS selectI1) 1);
-qed "Inf_is_Inf";
-
-Goal "is_Inf A inf --> Inf A = inf";
-  by (rtac impI 1);
-  by (rtac (is_Inf_uniq RS mp) 1);
-  by (rtac conjI 1);
-  by (rtac Inf_is_Inf 1);
-  by (assume_tac 1);
-qed "Inf_uniq";
-
-Goalw [Ex1_def] "ALL A. EX! inf::'a::clattice. is_Inf A inf";
-  by Safe_tac;
-  by (Step_tac 1);
-  by (Step_tac 1);
-  by (rtac Inf_is_Inf 1);
-  by (rtac (Inf_uniq RS mp RS sym) 1);
-  by (assume_tac 1);
-qed "ex1_Inf";
-
-
-Goalw [Sup_def] "is_Sup A (Sup A)";
-  by (rtac (ex_Sup RS spec RS selectI1) 1);
-qed "Sup_is_Sup";
-
-Goal "is_Sup A sup --> Sup A = sup";
-  by (rtac impI 1);
-  by (rtac (is_Sup_uniq RS mp) 1);
-  by (rtac conjI 1);
-  by (rtac Sup_is_Sup 1);
-  by (assume_tac 1);
-qed "Sup_uniq";
-
-Goalw [Ex1_def] "ALL A. EX! sup::'a::clattice. is_Sup A sup";
-  by Safe_tac;
-  by (Step_tac 1);
-  by (Step_tac 1);
-  by (rtac Sup_is_Sup 1);
-  by (rtac (Sup_uniq RS mp RS sym) 1);
-  by (assume_tac 1);
-qed "ex1_Sup";
-
-
-(* "Inf" yields g.l.bs, "Sup" yields l.u.bs. --- in pieces *)
-
-val prems = goalw thy [Inf_def] "x:A ==> Inf A [= x";
-  by (cut_facts_tac prems 1);
-  by (rtac someI2 1);
-  by (rtac Inf_is_Inf 1);
-  by (rewtac is_Inf_def);
-  by (Fast_tac 1);
-qed "Inf_lb";
-
-val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A";
-  by (rtac someI2 1);
-  by (rtac Inf_is_Inf 1);
-  by (rewtac is_Inf_def);
-  by (Step_tac 1);
-  by (Step_tac 1);
-  by (etac mp 1);
-  by (rtac ballI 1);
-  by (etac prem 1);
-qed "Inf_ub_lbs";
-
-
-val prems = goalw thy [Sup_def] "x:A ==> x [= Sup A";
-  by (cut_facts_tac prems 1);
-  by (rtac someI2 1);
-  by (rtac Sup_is_Sup 1);
-  by (rewtac is_Sup_def);
-  by (Fast_tac 1);
-qed "Sup_ub";
-
-val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z";
-  by (rtac someI2 1);
-  by (rtac Sup_is_Sup 1);
-  by (rewtac is_Sup_def);
-  by (Step_tac 1);
-  by (Step_tac 1);
-  by (etac mp 1);
-  by (rtac ballI 1);
-  by (etac prem 1);
-qed "Sup_lb_ubs";
-
-
-(** minorized Infs / majorized Sups **)
-
-Goal "(x [= Inf A) = (ALL y:A. x [= y)";
-  by (rtac iffI 1);
-  (*==>*)
-    by (rtac ballI 1);
-    by (rtac (le_trans RS mp) 1);
-    by (etac conjI 1);
-    by (etac Inf_lb 1);
-  (*<==*)
-    by (rtac Inf_ub_lbs 1);
-    by (Fast_tac 1);
-qed "le_Inf_eq";
-
-Goal "(Sup A [= x) = (ALL y:A. y [= x)";
-  by (rtac iffI 1);
-  (*==>*)
-    by (rtac ballI 1);
-    by (rtac (le_trans RS mp) 1);
-    by (rtac conjI 1);
-    by (etac Sup_ub 1);
-    by (assume_tac 1);
-  (*<==*)
-    by (rtac Sup_lb_ubs 1);
-    by (Fast_tac 1);
-qed "ge_Sup_eq";
-
-
-
-(** Subsets and limits **)
-
-Goal "A <= B --> Inf B [= Inf A";
-  by (rtac impI 1);
-  by (stac le_Inf_eq 1);
-  by (rewtac Ball_def);
-  by Safe_tac;
-  by (dtac subsetD 1);
-  by (assume_tac 1);
-  by (etac Inf_lb 1);
-qed "Inf_subset_antimon";
-
-Goal "A <= B --> Sup A [= Sup B";
-  by (rtac impI 1);
-  by (stac ge_Sup_eq 1);
-  by (rewtac Ball_def);
-  by Safe_tac;
-  by (dtac subsetD 1);
-  by (assume_tac 1);
-  by (etac Sup_ub 1);
-qed "Sup_subset_mon";
-
-
-(** singleton / empty limits **)
-
-Goal "Inf {x} = x";
-  by (rtac (Inf_uniq RS mp) 1);
-  by (rewtac is_Inf_def);
-  by Safe_tac;
-  by (rtac le_refl 1);
-  by (Fast_tac 1);
-qed "sing_Inf_eq";
-
-Goal "Sup {x} = x";
-  by (rtac (Sup_uniq RS mp) 1);
-  by (rewtac is_Sup_def);
-  by Safe_tac;
-  by (rtac le_refl 1);
-  by (Fast_tac 1);
-qed "sing_Sup_eq";
-
-
-Goal "Inf {} = Sup {x. True}";
-  by (rtac (Inf_uniq RS mp) 1);
-  by (rewtac is_Inf_def);
-  by Safe_tac;
-  by (rtac (sing_Sup_eq RS subst) 1);
-  back();
-  by (rtac (Sup_subset_mon RS mp) 1);
-  by (Fast_tac 1);
-qed "empty_Inf_eq";
-
-Goal "Sup {} = Inf {x. True}";
-  by (rtac (Sup_uniq RS mp) 1);
-  by (rewtac is_Sup_def);
-  by Safe_tac;
-  by (rtac (sing_Inf_eq RS subst) 1);
-  by (rtac (Inf_subset_antimon RS mp) 1);
-  by (Fast_tac 1);
-qed "empty_Sup_eq";
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Lattice/CLattice.thy
--- a/src/HOL/AxClasses/Lattice/CLattice.thy	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(*  Title:      CLattice.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Complete lattices are orders with infima and suprema of arbitrary
-subsets.
-
-TODO:
-  derive some more well-known theorems (e.g. ex_Inf == ex_Sup)
-*)
-
-CLattice = Order +
-
-axclass
-  clattice < partial_order
-  ex_Inf       "ALL A. EX inf. is_Inf A inf"
-  ex_Sup       "ALL A. EX sup. is_Sup A sup"
-
-constdefs
-  Inf           :: "'a::clattice set => 'a"
-  "Inf A == @inf. is_Inf A inf"
-
-  Sup           :: "'a::clattice set => 'a"
-  "Sup A == @sup. is_Sup A sup"
-
-end
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Lattice/LatInsts.ML
--- a/src/HOL/AxClasses/Lattice/LatInsts.ML	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,96 +0,0 @@
-
-
-Goal "Inf {x, y} = x && y";
-  by (rtac (Inf_uniq RS mp) 1);
-  by (stac bin_is_Inf_eq 1);
-  by (rtac inf_is_inf 1);
-qed "bin_Inf_eq";
-
-Goal "Sup {x, y} = x || y";
-  by (rtac (Sup_uniq RS mp) 1);
-  by (stac bin_is_Sup_eq 1);
-  by (rtac sup_is_sup 1);
-qed "bin_Sup_eq";
-
-
-
-(* Unions and limits *)
-
-Goal "Inf (A Un B) = Inf A && Inf B";
-  by (rtac (Inf_uniq RS mp) 1);
-  by (rewtac is_Inf_def);
-  by Safe_tac;
-
-  by (rtac (conjI RS (le_trans RS mp)) 1);
-  by (rtac inf_lb1 1);
-  by (etac Inf_lb 1);
-
-  by (rtac (conjI RS (le_trans RS mp)) 1);
-  by (rtac inf_lb2 1);
-  by (etac Inf_lb 1);
-
-  by (stac le_inf_eq 1);
-  by (rtac conjI 1);
-  by (rtac Inf_ub_lbs 1);
-  by (Fast_tac 1);
-  by (rtac Inf_ub_lbs 1);
-  by (Fast_tac 1);
-qed "Inf_Un_eq";
-
-Goal "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}";
-  by (rtac (Inf_uniq RS mp) 1);
-  by (rewtac is_Inf_def);
-  by Safe_tac;
-  (*level 3*)
-  by (rtac (conjI RS (le_trans RS mp)) 1);
-  by (etac Inf_lb 2);
-  by (rtac (sing_Inf_eq RS subst) 1);
-  by (rtac (Inf_subset_antimon RS mp) 1);
-  by (Fast_tac 1);
-  (*level 8*)
-  by (stac le_Inf_eq 1);
-  by Safe_tac;
-  by (stac le_Inf_eq 1);
-  by (Fast_tac 1);
-qed "Inf_UN_eq";
-
-
-
-Goal "Sup (A Un B) = Sup A || Sup B";
-  by (rtac (Sup_uniq RS mp) 1);
-  by (rewtac is_Sup_def);
-  by Safe_tac;
-
-  by (rtac (conjI RS (le_trans RS mp)) 1);
-  by (etac Sup_ub 1);
-  by (rtac sup_ub1 1);
-
-  by (rtac (conjI RS (le_trans RS mp)) 1);
-  by (etac Sup_ub 1);
-  by (rtac sup_ub2 1);
-
-  by (stac ge_sup_eq 1);
-  by (rtac conjI 1);
-  by (rtac Sup_lb_ubs 1);
-  by (Fast_tac 1);
-  by (rtac Sup_lb_ubs 1);
-  by (Fast_tac 1);
-qed "Sup_Un_eq";
-
-Goal "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}";
-  by (rtac (Sup_uniq RS mp) 1);
-  by (rewtac is_Sup_def);
-  by Safe_tac;
-  (*level 3*)
-  by (rtac (conjI RS (le_trans RS mp)) 1);
-  by (etac Sup_ub 1);
-  by (rtac (sing_Sup_eq RS subst) 1);
-  back();
-  by (rtac (Sup_subset_mon RS mp) 1);
-  by (Fast_tac 1);
-  (*level 8*)
-  by (stac ge_Sup_eq 1);
-  by Safe_tac;
-  by (stac ge_Sup_eq 1);
-  by (Fast_tac 1);
-qed "Sup_UN_eq";
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Lattice/LatInsts.thy
--- a/src/HOL/AxClasses/Lattice/LatInsts.thy	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(*  Title:      LatInsts.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Some lattice instantiations.
-*)
-
-LatInsts = LatPreInsts +
-
-
-(* linear orders are lattices *)
-
-instance
-  linear_order < lattice                (allI, exI, min_is_inf, max_is_sup)
-
-
-(* complete lattices are lattices *)
-
-instance
-  clattice < lattice                    (allI, exI, Inf_is_inf, Sup_is_sup)
-
-
-(* products of lattices are lattices *)
-
-instance
-  "*" :: (lattice, lattice) lattice     (allI, exI, prod_is_inf, prod_is_sup)
-
-instance
-  fun :: (term, lattice) lattice        (allI, exI, fun_is_inf, fun_is_sup)
-
-
-(* duals of lattices are lattices *)
-
-instance
-  dual :: (lattice) lattice             (allI, exI, dual_is_inf, dual_is_sup)
-
-(*FIXME bug workaround (see also OrdInsts.thy)*)
-instance
-  dual :: (linear_order) linear_order   (le_dual_linear)
-
-end
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Lattice/LatMorph.ML
--- a/src/HOL/AxClasses/Lattice/LatMorph.ML	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-
-
-(** monotone functions vs. "&&"- / "||"-semi-morphisms **)
-
-Goalw [is_mono_def] "is_mono f = (ALL x y. f (x && y) [= f x && f y)";
-  by Safe_tac;
-  (*==> (level 1)*)
-    by (stac le_inf_eq 1);
-    by (rtac conjI 1);
-    by (Step_tac 1);
-    by (Step_tac 1);
-    by (etac mp 1);
-    by (rtac inf_lb1 1);
-    by (Step_tac 1);
-    by (Step_tac 1);
-    by (etac mp 1);
-    by (rtac inf_lb2 1);
-  (*==> (level 11)*)
-    by (rtac (conjI RS (le_trans RS mp)) 1);
-    by (rtac inf_lb2 2);
-    by (subgoal_tac "x && y = x" 1);
-    by (etac subst 1);
-    by (Fast_tac 1);
-    by (stac inf_connect 1);
-    by (assume_tac 1);
-qed "mono_inf_eq";
-
-Goalw [is_mono_def] "is_mono f = (ALL x y. f x || f y [= f (x || y))";
-  by Safe_tac;
-  (*==> (level 1)*)
-    by (stac ge_sup_eq 1);
-    by (rtac conjI 1);
-    by (Step_tac 1);
-    by (Step_tac 1);
-    by (etac mp 1);
-    by (rtac sup_ub1 1);
-    by (Step_tac 1);
-    by (Step_tac 1);
-    by (etac mp 1);
-    by (rtac sup_ub2 1);
-  (*==> (level 11)*)
-    by (rtac (conjI RS (le_trans RS mp)) 1);
-    by (rtac sup_ub1 1);
-    by (subgoal_tac "x || y = y" 1);
-    by (etac subst 1);
-    by (Fast_tac 1);
-    by (stac sup_connect 1);
-    by (assume_tac 1);
-qed "mono_sup_eq";
-
-
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Lattice/LatMorph.thy
--- a/src/HOL/AxClasses/Lattice/LatMorph.thy	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(*  Title:      LatMorph.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Some lattice morphisms.
-
-TODO:
-  more morphisms (?)
-  more theorems
-*)
-
-LatMorph = LatInsts +
-
-constdefs
-  is_mono       :: "('a::le => 'b::le) => bool"
-  "is_mono f == ALL x y. x [= y --> f x [= f y"
-
-  is_inf_morph  :: "('a::lattice => 'b::lattice) => bool"
-  "is_inf_morph f == ALL x y. f (x && y) = f x && f y"
-
-  is_sup_morph  :: "('a::lattice => 'b::lattice) => bool"
-  "is_sup_morph f == ALL x y. f (x || y) = f x || f y"
-
-  is_Inf_morph  :: "('a::clattice => 'b::clattice) => bool"
-  "is_Inf_morph f == ALL A. f (Inf A) = Inf {f x |x. x:A}"
-
-  is_Sup_morph  :: "('a::clattice => 'b::clattice) => bool"
-  "is_Sup_morph f == ALL A. f (Sup A) = Sup {f x |x. x:A}"
-
-end
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Lattice/LatPreInsts.ML
--- a/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,74 +0,0 @@
-
-
-(** complete lattices **)
-
-Goal "is_inf x y (Inf {x, y})";
-  by (rtac (bin_is_Inf_eq RS subst) 1);
-  by (rtac Inf_is_Inf 1);
-qed "Inf_is_inf";
-
-Goal "is_sup x y (Sup {x, y})";
-  by (rtac (bin_is_Sup_eq RS subst) 1);
-  by (rtac Sup_is_Sup 1);
-qed "Sup_is_sup";
-
-
-
-(** product lattices **)
-
-(* pairs *)
-
-Goalw [is_inf_def, le_prod_def] "is_inf p q (fst p && fst q, snd p && snd q)";
-  by (Simp_tac 1);
-  by Safe_tac;
-  by (REPEAT_FIRST (fn i => resolve_tac [inf_lb1, inf_lb2, inf_ub_lbs] i ORELSE atac i));
-qed "prod_is_inf";
-
-Goalw [is_sup_def, le_prod_def] "is_sup p q (fst p || fst q, snd p || snd q)";
-  by (Simp_tac 1);
-  by Safe_tac;
-  by (REPEAT_FIRST (fn i => resolve_tac [sup_ub1, sup_ub2, sup_lb_ubs] i ORELSE atac i));
-qed "prod_is_sup";
-
-
-(* functions *)
-
-Goalw [is_inf_def, le_fun_def] "is_inf f g (%x. f x && g x)";
-  by Safe_tac;
-  by (rtac inf_lb1 1);
-  by (rtac inf_lb2 1);
-  by (rtac inf_ub_lbs 1);
-  by (REPEAT_FIRST (Fast_tac));
-qed "fun_is_inf";
-
-Goalw [is_sup_def, le_fun_def] "is_sup f g (%x. f x || g x)";
-  by Safe_tac;
-  by (rtac sup_ub1 1);
-  by (rtac sup_ub2 1);
-  by (rtac sup_lb_ubs 1);
-  by (REPEAT_FIRST (Fast_tac));
-qed "fun_is_sup";
-
-
-
-(** dual lattices **)
-
-Goalw [is_inf_def, le_dual_def] "is_inf x y (Abs_dual (Rep_dual x || Rep_dual y))";
-  by (stac Abs_dual_inverse' 1);
-  by Safe_tac;
-  by (rtac sup_ub1 1);
-  by (rtac sup_ub2 1);
-  by (rtac sup_lb_ubs 1);
-  by (assume_tac 1);
-  by (assume_tac 1);
-qed "dual_is_inf";
-
-Goalw [is_sup_def, le_dual_def] "is_sup x y (Abs_dual (Rep_dual x && Rep_dual y))";
-  by (stac Abs_dual_inverse' 1);
-  by Safe_tac;
-  by (rtac inf_lb1 1);
-  by (rtac inf_lb2 1);
-  by (rtac inf_ub_lbs 1);
-  by (assume_tac 1);
-  by (assume_tac 1);
-qed "dual_is_sup";
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Lattice/LatPreInsts.thy
--- a/src/HOL/AxClasses/Lattice/LatPreInsts.thy	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-(*  Title:      LatPreInsts.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-*)
-
-LatPreInsts = OrdInsts + Lattice + CLattice
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Lattice/Lattice.ML
--- a/src/HOL/AxClasses/Lattice/Lattice.ML	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,276 +0,0 @@
-
-context HOL.thy;
-
-Goalw [Ex_def] "EX x. P x ==> P (@x. P x)";
-  by (assume_tac 1);
-qed "selectI1";
-
-context thy;
-
-
-
-(** basic properties of "&&" and "||" **)
-
-(* unique existence *)
-
-Goalw [inf_def] "is_inf x y (x && y)";
-  by (rtac (ex_inf RS spec RS spec RS selectI1) 1);
-qed "inf_is_inf";
-
-Goal "is_inf x y inf --> x && y = inf";
-  by (rtac impI 1);
-  by (rtac (is_inf_uniq RS mp) 1);
-  by (rtac conjI 1);
-  by (rtac inf_is_inf 1);
-  by (assume_tac 1);
-qed "inf_uniq";
-
-Goalw [Ex1_def] "ALL x y. EX! inf::'a::lattice. is_inf x y inf";
-  by Safe_tac;
-  by (Step_tac 1);
-  by (Step_tac 1);
-  by (rtac inf_is_inf 1);
-  by (rtac (inf_uniq RS mp RS sym) 1);
-  by (assume_tac 1);
-qed "ex1_inf";
-
-
-Goalw [sup_def] "is_sup x y (x || y)";
-  by (rtac (ex_sup RS spec RS spec RS selectI1) 1);
-qed "sup_is_sup";
-
-Goal "is_sup x y sup --> x || y = sup";
-  by (rtac impI 1);
-  by (rtac (is_sup_uniq RS mp) 1);
-  by (rtac conjI 1);
-  by (rtac sup_is_sup 1);
-  by (assume_tac 1);
-qed "sup_uniq";
-
-Goalw [Ex1_def] "ALL x y. EX! sup::'a::lattice. is_sup x y sup";
-  by Safe_tac;
-  by (Step_tac 1);
-  by (Step_tac 1);
-  by (rtac sup_is_sup 1);
-  by (rtac (sup_uniq RS mp RS sym) 1);
-  by (assume_tac 1);
-qed "ex1_sup";
-
-
-(* "&&" yields g.l.bs, "||" yields l.u.bs. --- in pieces *)
-
-val tac =
-  cut_facts_tac [inf_is_inf] 1 THEN
-  rewrite_goals_tac [inf_def, is_inf_def] THEN
-  Fast_tac 1;
-
-Goal "x && y [= x";
-  by tac;
-qed "inf_lb1";
-
-Goal "x && y [= y";
-  by tac;
-qed "inf_lb2";
-
-val prems = goal thy "[| z [= x; z [= y |] ==> z [= x && y";
-  by (cut_facts_tac prems 1);
-  by tac;
-qed "inf_ub_lbs";
-
-
-val tac =
-  cut_facts_tac [sup_is_sup] 1 THEN
-  rewrite_goals_tac [sup_def, is_sup_def] THEN
-  Fast_tac 1;
-
-Goal "x [= x || y";
-  by tac;
-qed "sup_ub1";
-
-Goal "y [= x || y";
-  by tac;
-qed "sup_ub2";
-
-val prems = goal thy "[| x [= z; y [= z |] ==> x || y [= z";
-  by (cut_facts_tac prems 1);
-  by tac;
-qed "sup_lb_ubs";
-
-
-
-(** some equations concerning "&&" and "||" vs. "[=" **)
-
-(* the Connection Theorems: "[=" expressed via "&&" or "||" *)
-
-Goal "(x && y = x) = (x [= y)";
-  by (rtac iffI 1);
-  (*==>*)
-    by (etac subst 1);
-    by (rtac inf_lb2 1);
-  (*<==*)
-    by (rtac (inf_uniq RS mp) 1);
-    by (rewtac is_inf_def);
-    by (REPEAT_FIRST (rtac conjI));
-    by (rtac le_refl 1);
-    by (assume_tac 1);
-    by (Fast_tac 1);
-qed "inf_connect";
-
-Goal "(x || y = y) = (x [= y)";
-  by (rtac iffI 1);
-  (*==>*)
-    by (etac subst 1);
-    by (rtac sup_ub1 1);
-  (*<==*)
-    by (rtac (sup_uniq RS mp) 1);
-    by (rewtac is_sup_def);
-    by (REPEAT_FIRST (rtac conjI));
-    by (assume_tac 1);
-    by (rtac le_refl 1);
-    by (Fast_tac 1);
-qed "sup_connect";
-
-
-(* minorized infs / majorized sups *)
-
-Goal "(x [= y && z) = (x [= y & x [= z)";
-  by (rtac iffI 1);
-  (*==> (level 1)*)
-    by (cut_facts_tac [inf_lb1, inf_lb2] 1);
-    by (rtac conjI 1);
-    by (rtac (le_trans RS mp) 1);
-    by (etac conjI 1);
-    by (assume_tac 1);
-    by (rtac (le_trans RS mp) 1);
-    by (etac conjI 1);
-    by (assume_tac 1);
-  (*<== (level 9)*)
-    by (etac conjE 1);
-    by (etac inf_ub_lbs 1);
-    by (assume_tac 1);
-qed "le_inf_eq";
-
-Goal "(x || y [= z) = (x [= z & y [= z)";
-  by (rtac iffI 1);
-  (*==> (level 1)*)
-    by (cut_facts_tac [sup_ub1, sup_ub2] 1);
-    by (rtac conjI 1);
-    by (rtac (le_trans RS mp) 1);
-    by (etac conjI 1);
-    by (assume_tac 1);
-    by (rtac (le_trans RS mp) 1);
-    by (etac conjI 1);
-    by (assume_tac 1);
-  (*<== (level 9)*)
-    by (etac conjE 1);
-    by (etac sup_lb_ubs 1);
-    by (assume_tac 1);
-qed "ge_sup_eq";
-
-
-(** algebraic properties of "&&" and "||": A, C, I, AB **)
-
-(* associativity *)
-
-Goal "(x && y) && z = x && (y && z)";
-  by (stac (inf_uniq RS mp RS sym) 1);
-  back();
-  back();
-  back();
-  back();
-  back();
-  back();
-  back();
-  back();
-  by (rtac refl 2);
-  by (rtac (is_inf_assoc RS mp) 1);
-  by (REPEAT_FIRST (rtac conjI));
-  by (REPEAT_FIRST (rtac inf_is_inf));
-qed "inf_assoc";
-
-Goal "(x || y) || z = x || (y || z)";
-  by (stac (sup_uniq RS mp RS sym) 1);
-  back();
-  back();
-  back();
-  back();
-  back();
-  back();
-  back();
-  back();
-  by (rtac refl 2);
-  by (rtac (is_sup_assoc RS mp) 1);
-  by (REPEAT_FIRST (rtac conjI));
-  by (REPEAT_FIRST (rtac sup_is_sup));
-qed "sup_assoc";
-
-
-(* commutativity *)
-
-Goalw [inf_def] "x && y = y && x";
-  by (stac (is_inf_commut RS ext) 1);
-  by (rtac refl 1);
-qed "inf_commut";
-
-Goalw [sup_def] "x || y = y || x";
-  by (stac (is_sup_commut RS ext) 1);
-  by (rtac refl 1);
-qed "sup_commut";
-
-
-(* idempotency *)
-
-Goal "x && x = x";
-  by (stac inf_connect 1);
-  by (rtac le_refl 1);
-qed "inf_idemp";
-
-Goal "x || x = x";
-  by (stac sup_connect 1);
-  by (rtac le_refl 1);
-qed "sup_idemp";
-
-
-(* absorption *)
-
-Goal "x || (x && y) = x";
-  by (stac sup_commut 1);
-  by (stac sup_connect 1);
-  by (rtac inf_lb1 1);
-qed "sup_inf_absorb";
-
-Goal "x && (x || y) = x";
-  by (stac inf_connect 1);
-  by (rtac sup_ub1 1);
-qed "inf_sup_absorb";
-
-
-(* monotonicity *)
-
-val prems = goal thy "[| a [= b; x [= y |] ==> a && x [= b && y";
-  by (cut_facts_tac prems 1);
-  by (stac le_inf_eq 1);
-  by (rtac conjI 1);
-  by (rtac (le_trans RS mp) 1);
-  by (rtac conjI 1);
-  by (rtac inf_lb1 1);
-  by (assume_tac 1);
-  by (rtac (le_trans RS mp) 1);
-  by (rtac conjI 1);
-  by (rtac inf_lb2 1);
-  by (assume_tac 1);
-qed "inf_mon";
-
-val prems = goal thy "[| a [= b; x [= y |] ==> a || x [= b || y";
-  by (cut_facts_tac prems 1);
-  by (stac ge_sup_eq 1);
-  by (rtac conjI 1);
-  by (rtac (le_trans RS mp) 1);
-  by (rtac conjI 1);
-  by (assume_tac 1);
-  by (rtac sup_ub1 1);
-  by (rtac (le_trans RS mp) 1);
-  by (rtac conjI 1);
-  by (assume_tac 1);
-  by (rtac sup_ub2 1);
-qed "sup_mon";
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Lattice/Lattice.thy
--- a/src/HOL/AxClasses/Lattice/Lattice.thy	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(*  Title:      Lattice.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Lattices are orders with binary (finitary) infima and suprema.
-*)
-
-Lattice = Order +
-
-axclass
-  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"
-
-consts
-  "&&"          :: "['a::lattice, 'a] => 'a"       (infixl 70)
-  "||"          :: "['a::lattice, 'a] => 'a"       (infixl 65)
-
-defs
-  inf_def       "x && y == @inf. is_inf x y inf"
-  sup_def       "x || y == @sup. is_sup x y sup"
-
-end
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Lattice/OrdDefs.ML
--- a/src/HOL/AxClasses/Lattice/OrdDefs.ML	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,87 +0,0 @@
-
-
-(** lifting of quasi / partial orders **)
-
-(* pairs *)
-
-Goalw [le_prod_def] "x [= (x::'a::quasi_order*'b::quasi_order)";
-  by (rtac conjI 1);
-  by (rtac le_refl 1);
-  by (rtac le_refl 1);
-qed "le_prod_refl";
-
-Goalw [le_prod_def] "x [= y & y [= z --> x [= (z::'a::quasi_order*'b::quasi_order)";
-  by Safe_tac;
-  by (etac (conjI RS (le_trans RS mp)) 1);
-  by (assume_tac 1);
-  by (etac (conjI RS (le_trans RS mp)) 1);
-  by (assume_tac 1);
-qed "le_prod_trans";
-
-Goalw [le_prod_def] "x [= y & y [= x --> x = (y::'a::partial_order*'b::partial_order)";
-  by Safe_tac;
-  by (stac Pair_fst_snd_eq 1);
-  by (rtac conjI 1);
-  by (etac (conjI RS (le_antisym RS mp)) 1);
-  by (assume_tac 1);
-  by (etac (conjI RS (le_antisym RS mp)) 1);
-  by (assume_tac 1);
-qed "le_prod_antisym";
-
-
-(* functions *)
-
-Goalw [le_fun_def] "f [= (f::'a=>'b::quasi_order)";
-  by (rtac allI 1);
-  by (rtac le_refl 1);
-qed "le_fun_refl";
-
-Goalw [le_fun_def] "f [= g & g [= h --> f [= (h::'a=>'b::quasi_order)";
-  by Safe_tac;
-  by (rtac (le_trans RS mp) 1);
-  by (Fast_tac 1);
-qed "le_fun_trans";
-
-Goalw [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::partial_order)";
-  by Safe_tac;
-  by (rtac ext 1);
-  by (rtac (le_antisym RS mp) 1);
-  by (Fast_tac 1);
-qed "le_fun_antisym";
-
-
-
-(** duals **)
-
-(*"'a dual" is even an isotype*)
-Goal "Rep_dual (Abs_dual y) = y";
-  by (rtac Abs_dual_inverse 1);
-  by (rewtac dual_def);
-  by (Fast_tac 1);
-qed "Abs_dual_inverse'";
-
-
-Goalw [le_dual_def] "x [= (x::'a::quasi_order dual)";
-  by (rtac le_refl 1);
-qed "le_dual_refl";
-
-Goalw [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)";
-  by (rtac impI 1);
-  by (rtac (le_trans RS mp) 1);
-  by (Blast_tac 1);
-qed "le_dual_trans";
-
-Goalw [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)";
-  by Safe_tac;
-  by (rtac (Rep_dual_inverse RS subst) 1);
-  by (rtac sym 1);
-  by (rtac (Rep_dual_inverse RS subst) 1);
-  by (rtac arg_cong 1);
-  back();
-  by (etac (conjI RS (le_antisym RS mp)) 1);
-  by (assume_tac 1);
-qed "le_dual_antisym";
-
-Goalw [le_dual_def] "x [= y | y [= (x::'a::linear_order dual)";
-  by (rtac le_linear 1);
-qed "le_dual_linear";
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Lattice/OrdDefs.thy
--- a/src/HOL/AxClasses/Lattice/OrdDefs.thy	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(*  Title:      OrdDefs.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Some overloaded definitions.
-*)
-
-OrdDefs = Order + Prod +
-
-
-(* binary / general products *)
-
-instance
-  "*" :: (le, le) le
-
-instance
-  fun :: (term, le) le
-
-defs
-  le_prod_def   "p [= q == fst p [= fst q & snd p [= snd q"
-  le_fun_def    "f [= g == ALL x. f x [= g x"
-
-
-(* duals *)
-
-typedef
-  'a dual = "{x::'a. True}"
-
-instance
-  dual :: (le) le
-
-defs
-  le_dual_def   "x [= y == Rep_dual y [= Rep_dual x"
-
-end
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Lattice/Order.ML
--- a/src/HOL/AxClasses/Lattice/Order.ML	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,171 +0,0 @@
-
-
-(** basic properties of limits **)
-
-(* uniqueness *)
-
-val tac =
-  rtac impI 1 THEN
-  rtac (le_antisym RS mp) 1 THEN
-  Fast_tac 1;
-
-
-Goalw [is_inf_def] "is_inf x y inf & is_inf x y inf' --> inf = inf'";
-  by tac;
-qed "is_inf_uniq";
-
-Goalw [is_sup_def] "is_sup x y sup & is_sup x y sup' --> sup = sup'";
-  by tac;
-qed "is_sup_uniq";
-
-
-Goalw [is_Inf_def] "is_Inf A inf & is_Inf A inf' --> inf = inf'";
-  by tac;
-qed "is_Inf_uniq";
-
-Goalw [is_Sup_def] "is_Sup A sup & is_Sup A sup' --> sup = sup'";
-  by tac;
-qed "is_Sup_uniq";
-
-
-
-(* commutativity *)
-
-Goalw [is_inf_def] "is_inf x y inf = is_inf y x inf";
-  by (Fast_tac 1);
-qed "is_inf_commut";
-
-Goalw [is_sup_def] "is_sup x y sup = is_sup y x sup";
-  by (Fast_tac 1);
-qed "is_sup_commut";
-
-
-(* associativity *)
-
-Goalw [is_inf_def] "is_inf x y xy & is_inf y z yz & is_inf xy z xyz --> is_inf x yz xyz";
-  by Safe_tac;
-  (*level 1*)
-    by (rtac (le_trans RS mp) 1);
-    by (etac conjI 1);
-    by (assume_tac 1);
-  (*level 4*)
-    by (Step_tac 1);
-    back();
-    by (etac mp 1);
-    by (rtac conjI 1);
-    by (rtac (le_trans RS mp) 1);
-    by (etac conjI 1);
-    by (assume_tac 1);
-    by (assume_tac 1);
-  (*level 11*)
-    by (Step_tac 1);
-    back();
-    back();
-    by (etac mp 1);
-    by (rtac conjI 1);
-    by (Step_tac 1);
-    by (etac mp 1);
-    by (etac conjI 1);
-    by (rtac (le_trans RS mp) 1);
-    by (etac conjI 1);
-    by (assume_tac 1);
-    by (rtac (le_trans RS mp) 1);
-    by (etac conjI 1);
-    back();     (* !! *)
-    by (assume_tac 1);
-qed "is_inf_assoc";
-
-
-Goalw [is_sup_def] "is_sup x y xy & is_sup y z yz & is_sup xy z xyz --> is_sup x yz xyz";
-  by Safe_tac;
-  (*level 1*)
-    by (rtac (le_trans RS mp) 1);
-    by (etac conjI 1);
-    by (assume_tac 1);
-  (*level 4*)
-    by (Step_tac 1);
-    back();
-    by (etac mp 1);
-    by (rtac conjI 1);
-    by (rtac (le_trans RS mp) 1);
-    by (etac conjI 1);
-    by (assume_tac 1);
-    by (assume_tac 1);
-  (*level 11*)
-    by (Step_tac 1);
-    back();
-    back();
-    by (etac mp 1);
-    by (rtac conjI 1);
-    by (Step_tac 1);
-    by (etac mp 1);
-    by (etac conjI 1);
-    by (rtac (le_trans RS mp) 1);
-    by (etac conjI 1);
-    back();     (* !! *)
-    by (assume_tac 1);
-    by (rtac (le_trans RS mp) 1);
-    by (etac conjI 1);
-    by (assume_tac 1);
-qed "is_sup_assoc";
-
-
-(** limits in linear orders **)
-
-Goalw [minimum_def, is_inf_def] "is_inf (x::'a::linear_order) y (minimum x y)";
-  by (stac split_if 1);
-  by (REPEAT_FIRST (resolve_tac [conjI, impI]));
-  (*case "x [= y"*)
-    by (rtac le_refl 1);
-    by (assume_tac 1);
-    by (Fast_tac 1);
-  (*case "~ x [= y"*)
-    by (rtac (le_linear RS disjE) 1);
-    by (assume_tac 1);
-    by (etac notE 1);
-    by (assume_tac 1);
-    by (rtac le_refl 1);
-    by (Fast_tac 1);
-qed "min_is_inf";
-
-Goalw [maximum_def, is_sup_def] "is_sup (x::'a::linear_order) y (maximum x y)";
-  by (stac split_if 1);
-  by (REPEAT_FIRST (resolve_tac [conjI, impI]));
-  (*case "x [= y"*)
-    by (assume_tac 1);
-    by (rtac le_refl 1);
-    by (Fast_tac 1);
-  (*case "~ x [= y"*)
-    by (rtac le_refl 1);
-    by (rtac (le_linear RS disjE) 1);
-    by (assume_tac 1);
-    by (etac notE 1);
-    by (assume_tac 1);
-    by (Fast_tac 1);
-qed "max_is_sup";
-
-
-
-(** general vs. binary limits **)
-
-Goalw [is_inf_def, is_Inf_def] "is_Inf {x, y} inf = is_inf x y inf";
-  by (rtac iffI 1);
-  (*==>*)
-    by (Fast_tac 1);
-  (*<==*)
-    by Safe_tac;
-    by (Step_tac 1);
-    by (etac mp 1);
-    by (Fast_tac 1);
-qed "bin_is_Inf_eq";
-
-Goalw [is_sup_def, is_Sup_def] "is_Sup {x, y} sup = is_sup x y sup";
-  by (rtac iffI 1);
-  (*==>*)
-    by (Fast_tac 1);
-  (*<==*)
-    by Safe_tac;
-    by (Step_tac 1);
-    by (etac mp 1);
-    by (Fast_tac 1);
-qed "bin_is_Sup_eq";
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Lattice/Order.thy
--- a/src/HOL/AxClasses/Lattice/Order.thy	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-(*  Title:      Order.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Basic theory of orders (quasi orders, partial orders, linear orders)
-and limits (inf, sup, min, max).
-*)
-
-Order = HOL + Set +
-
-
-(** class definitions **)
-
-(* syntax for orders *)
-
-axclass
-  le < term
-
-consts
-  "[="          :: "['a::le, 'a] => bool"             (infixl 50)
-
-
-(* quasi orders *)
-
-axclass
-  quasi_order < le
-  le_refl       "x [= x"
-  le_trans      "x [= y & y [= z --> x [= z"
-
-
-(* partial orders *)
-
-axclass
-  partial_order < quasi_order
-  le_antisym    "x [= y & y [= x --> x = y"
-
-
-(* linear orders *)
-
-axclass
-  linear_order < partial_order
-  le_linear     "x [= y | y [= x"
-
-
-
-(** limits **)
-
-(* infima and suprema (on orders) *)
-
-consts
-  (*binary*)
-  is_inf        :: "['a::partial_order, 'a, 'a] => bool"
-  is_sup        :: "['a::partial_order, 'a, 'a] => bool"
-  (*general*)
-  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 ==
-                   inf [= x & inf [= y &
-                   (ALL lb. lb [= x & lb [= y --> lb [= inf)"
-  is_sup_def    "is_sup x y sup ==
-                   x [= sup & y [= sup &
-                   (ALL ub. x [= ub & y [= ub --> sup [= ub)"
-  is_Inf_def    "is_Inf A inf ==
-                   (ALL x:A. inf [= x) &
-                   (ALL lb. (ALL x:A. lb [= x) --> lb [= inf)"
-  is_Sup_def    "is_Sup A sup ==
-                   (ALL x:A. x [= sup) &
-                   (ALL ub. (ALL x:A. x [= ub) --> sup [= ub)"
-
-
-
-(* binary minima and maxima (on linear_orders) *)
-
-constdefs
-  minimum      :: "['a::linear_order, 'a] => 'a"
-  "minimum x y == (if x [= y then x else y)"
-
-  maximum      :: "['a::linear_order, 'a] => 'a"
-  "maximum x y == (if x [= y then y else x)"
-
-end
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Lattice/ROOT.ML
--- a/src/HOL/AxClasses/Lattice/ROOT.ML	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(*  Title:      HOL/AxClasses/Lattice/ROOT.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Basic theory of lattices and orders via axiomatic type classes.
-*)
-
-open AxClass;
-
-reset eta_contract;
-set show_types;
-set show_sorts;
-
-time_use_thy "Order";
-time_use_thy "OrdDefs";
-time_use_thy "OrdInsts";
-
-time_use_thy "Lattice";
-time_use_thy "CLattice";
-
-time_use_thy "LatPreInsts";
-time_use_thy "LatInsts";
-
-time_use_thy "LatMorph";
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Oct 03 18:30:56 2000 +0200
+++ b/src/HOL/IsaMakefile	Tue Oct 03 18:34:20 2000 +0200
@@ -8,13 +8,12 @@
 
 default: HOL
 images: HOL HOL-Real TLA
-test: HOL-Isar_examples HOL-Induct HOL-Lambda HOL-ex HOL-Subst HOL-IMP HOL-IMPP \
-  HOL-NumberTheory HOL-Hoare HOL-Lex HOL-Algebra \
-  HOL-Auth HOL-UNITY HOL-Modelcheck \
-  HOL-Prolog HOL-W0 HOL-MiniML HOL-BCV HOL-MicroJava \
-  HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
-  HOL-AxClasses-Tutorial HOL-Real-ex \
-  HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory
+
+test: HOL-Isar_examples HOL-Induct HOL-Lambda HOL-AxClasses HOL-ex HOL-Subst HOL-IMP \
+  HOL-IMPP HOL-NumberTheory HOL-Hoare HOL-Lex HOL-Algebra HOL-Auth \
+  HOL-UNITY HOL-Modelcheck HOL-Prolog HOL-W0 HOL-MiniML HOL-BCV \
+  HOL-MicroJava HOL-IOA HOL-Real-ex HOL-Real-HahnBanach \
+  TLA-Inc TLA-Buffer TLA-Memory
 
 all: images test
 
@@ -398,42 +397,13 @@
 	@$(ISATOOL) usedir $(OUT)/HOL IOA
 
 
-## HOL-AxClasses-Group
-
-HOL-AxClasses-Group: HOL $(LOG)/HOL-AxClasses-Group.gz
+## HOL-AxClasses
 
-$(LOG)/HOL-AxClasses-Group.gz: $(OUT)/HOL AxClasses/Group/Group.ML \
-  AxClasses/Group/Group.thy AxClasses/Group/GroupDefs.ML \
-  AxClasses/Group/GroupDefs.thy AxClasses/Group/GroupInsts.thy \
-  AxClasses/Group/Monoid.thy AxClasses/Group/MonoidGroupInsts.thy \
-  AxClasses/Group/ROOT.ML AxClasses/Group/Sigs.thy
-	@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group
-
-
-## HOL-AxClasses-Lattice
-
-HOL-AxClasses-Lattice: HOL $(LOG)/HOL-AxClasses-Lattice.gz
+HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz
 
-$(LOG)/HOL-AxClasses-Lattice.gz: $(OUT)/HOL AxClasses/Lattice/CLattice.ML \
-  AxClasses/Lattice/CLattice.thy AxClasses/Lattice/LatInsts.ML \
-  AxClasses/Lattice/LatInsts.thy AxClasses/Lattice/LatMorph.ML \
-  AxClasses/Lattice/LatMorph.thy AxClasses/Lattice/LatPreInsts.ML \
-  AxClasses/Lattice/LatPreInsts.thy AxClasses/Lattice/Lattice.ML \
-  AxClasses/Lattice/Lattice.thy AxClasses/Lattice/OrdDefs.ML \
-  AxClasses/Lattice/OrdDefs.thy AxClasses/Lattice/OrdInsts.thy \
-  AxClasses/Lattice/Order.ML AxClasses/Lattice/Order.thy \
-  AxClasses/Lattice/ROOT.ML
-	@$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice
-
-
-## HOL-AxClasses-Tutorial
-
-HOL-AxClasses-Tutorial: HOL $(LOG)/HOL-AxClasses-Tutorial.gz
-
-$(LOG)/HOL-AxClasses-Tutorial.gz: $(OUT)/HOL \
-  AxClasses/Tutorial/Group.thy AxClasses/Tutorial/Product.thy \
-  AxClasses/Tutorial/ROOT.ML AxClasses/Tutorial/Semigroups.thy
-	@$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial
+$(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/Group.thy \
+  AxClasses/Product.thy AxClasses/ROOT.ML AxClasses/Semigroups.thy
+	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
 
 
 ## HOL-ex
@@ -531,8 +501,7 @@
 		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
 		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
 		$(LOG)/HOL-BCV.gz $(LOG)/HOL-MicroJava.gz \
-		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses-Group.gz \
-		$(LOG)/HOL-AxClasses-Lattice.gz	\
-		$(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Real-ex.gz \
+		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
+		$(LOG)/HOL-Real-ex.gz \
 		$(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \
 		$(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz