# HG changeset patch
# User clasohm
# Date 826637974 -3600
# Node ID 6d66b59f94a97aa886848be8a2075b9159ab7ca6
# Parent  dbecd983863f1b9aaedf5239bba1b535f96ba26e
added constdefs section

diff -r dbecd983863f -r 6d66b59f94a9 src/HOL/AxClasses/Lattice/CLattice.thy
--- a/src/HOL/AxClasses/Lattice/CLattice.thy	Tue Mar 12 14:38:58 1996 +0100
+++ b/src/HOL/AxClasses/Lattice/CLattice.thy	Tue Mar 12 14:39:34 1996 +0100
@@ -16,12 +16,11 @@
   ex_Inf       "ALL A. EX inf. is_Inf A inf"
   ex_Sup       "ALL A. EX sup. is_Sup A sup"
 
-consts
+constdefs
   Inf           :: "'a::clattice set => 'a"
-  Sup           :: "'a::clattice set => 'a"
+  "Inf A == @inf. is_Inf A inf"
 
-defs
-  Inf_def       "Inf A == @inf. is_Inf A inf"
-  Sup_def       "Sup A == @sup. is_Sup A sup"
+  Sup           :: "'a::clattice set => 'a"
+  "Sup A == @sup. is_Sup A sup"
 
 end
diff -r dbecd983863f -r 6d66b59f94a9 src/HOL/AxClasses/Lattice/LatMorph.thy
--- a/src/HOL/AxClasses/Lattice/LatMorph.thy	Tue Mar 12 14:38:58 1996 +0100
+++ b/src/HOL/AxClasses/Lattice/LatMorph.thy	Tue Mar 12 14:39:34 1996 +0100
@@ -11,18 +11,20 @@
 
 LatMorph = LatInsts +
 
-consts
+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_sup_morph  :: "('a::lattice => 'b::lattice) => bool"
-  is_Inf_morph  :: "('a::clattice => 'b::clattice) => bool"
-  is_Sup_morph  :: "('a::clattice => 'b::clattice) => bool"
+  "is_inf_morph f == ALL x y. f (x && y) = f x && f y"
 
-defs
-  is_mono_def       "is_mono f == ALL x y. x [= y --> f x [= f y"
-  is_inf_morph_def  "is_inf_morph f == ALL x y. f (x && y) = f x && f y"
-  is_sup_morph_def  "is_sup_morph f == ALL x y. f (x || y) = f x || f y"
-  is_Inf_morph_def  "is_Inf_morph f == ALL A. f (Inf A) = Inf {f x |x. x:A}"
-  is_Sup_morph_def  "is_Sup_morph f == ALL A. f (Sup A) = Sup {f x |x. x:A}"
+  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 dbecd983863f -r 6d66b59f94a9 src/HOL/AxClasses/Lattice/LatPreInsts.ML
--- a/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Tue Mar 12 14:38:58 1996 +0100
+++ b/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Tue Mar 12 14:39:34 1996 +0100
@@ -21,13 +21,13 @@
 (* pairs *)
 
 goalw thy [is_inf_def, le_prod_def] "is_inf p q (fst p && fst q, snd p && snd q)";
-  by (simp_tac prod_ss 1);
+  by (Simp_tac 1);
   by (safe_tac HOL_cs);
   by (REPEAT_FIRST (fn i => resolve_tac [inf_lb1, inf_lb2, inf_ub_lbs] i ORELSE atac i));
 qed "prod_is_inf";
 
 goalw thy [is_sup_def, le_prod_def] "is_sup p q (fst p || fst q, snd p || snd q)";
-  by (simp_tac prod_ss 1);
+  by (Simp_tac 1);
   by (safe_tac HOL_cs);
   by (REPEAT_FIRST (fn i => resolve_tac [sup_ub1, sup_ub2, sup_lb_ubs] i ORELSE atac i));
 qed "prod_is_sup";
diff -r dbecd983863f -r 6d66b59f94a9 src/HOL/AxClasses/Lattice/Order.thy
--- a/src/HOL/AxClasses/Lattice/Order.thy	Tue Mar 12 14:38:58 1996 +0100
+++ b/src/HOL/AxClasses/Lattice/Order.thy	Tue Mar 12 14:39:34 1996 +0100
@@ -70,14 +70,14 @@
                    (ALL ub. (ALL x:A. x [= ub) --> sup [= ub)"
 
 
+
 (* binary minima and maxima (on lin_orders) *)
 
-consts
+constdefs
   minimum      :: "['a::lin_order, 'a] => 'a"
-  maximum      :: "['a::lin_order, 'a] => 'a"
+  "minimum x y == (if x [= y then x else y)"
 
-defs
-  minimum_def  "minimum x y == (if x [= y then x else y)"
-  maximum_def  "maximum x y == (if x [= y then y else x)"
+  maximum      :: "['a::lin_order, 'a] => 'a"
+  "maximum x y == (if x [= y then y else x)"
 
 end
diff -r dbecd983863f -r 6d66b59f94a9 src/HOL/AxClasses/Tutorial/Semigroups.thy
--- a/src/HOL/AxClasses/Tutorial/Semigroups.thy	Tue Mar 12 14:38:58 1996 +0100
+++ b/src/HOL/AxClasses/Tutorial/Semigroups.thy	Tue Mar 12 14:39:34 1996 +0100
@@ -10,10 +10,10 @@
 consts
   "<+>"         :: "['a, 'a] => 'a"             (infixl 65)
   "<*>"         :: "['a, 'a] => 'a"             (infixl 70)
+
+constdefs
   assoc         :: "(['a, 'a] => 'a) => bool"
-
-defs
-  assoc_def     "assoc f == ALL x y z. f (f x y) z = f x (f y z)"
+  "assoc f == ALL x y z. f (f x y) z = f x (f y z)"
 
 
 (* semigroups with op <+> *)