# HG changeset patch
# User nipkow
# Date 962987267 -7200
# Node ID fb4186e201482a85304be5cc4a38a3058ea23b5c
# Parent  0b8e87bb91d98946ecb534ca5ee5f0c52c83d194
added type classes to constant's type

diff -r 0b8e87bb91d9 -r fb4186e20148 src/HOL/Algebra/poly/PolyHomo.thy
--- a/src/HOL/Algebra/poly/PolyHomo.thy	Fri Jul 07 17:15:17 2000 +0200
+++ b/src/HOL/Algebra/poly/PolyHomo.thy	Fri Jul 07 18:27:47 2000 +0200
@@ -13,7 +13,7 @@
 
 consts
   EVAL2	:: ('a::ringS => 'b) => 'b => 'a up => 'b::ringS
-  EVAL	:: 'a => 'a up => 'a
+  EVAL	:: 'a::ringS => 'a up => 'a
 
 defs
   EVAL2_def	"EVAL2 phi a p == SUM (deg p) (%i. phi (coeff i p) * a ^ i)"
diff -r 0b8e87bb91d9 -r fb4186e20148 src/HOL/BCV/DFAandWTI.thy
--- a/src/HOL/BCV/DFAandWTI.thy	Fri Jul 07 17:15:17 2000 +0200
+++ b/src/HOL/BCV/DFAandWTI.thy	Fri Jul 07 18:27:47 2000 +0200
@@ -12,13 +12,13 @@
 
 constdefs
 
- stable :: (nat => 's => 's option) => (nat => nat list) => nat => 's os => bool
+ stable :: (nat => 's::ord => 's option) => (nat => nat list) => nat => 's os => bool
 "stable step succs p sos ==
  !s. sos!p = Some s --> (? t. step p s = Some(t) &
                               (!q:set(succs p). Some t <= sos!q))"
 
  wti_is_fix_step ::
-   "(nat => 's => 's option)
+   "(nat => 's::ord => 's option)
     => (nat => 's os => bool)
     => (nat => nat list)
     => nat => 's set => bool"
@@ -30,7 +30,7 @@
 "welltyping wti tos == !p<size(tos). wti p tos"
 
  is_dfa ::  ('s os => bool)
-            => (nat => 's => 's option)
+            => (nat => 's::ord => 's option)
             => (nat => nat list)
             => nat => 's set => bool
 "is_dfa dfa step succs n L == !sos : listsn n (option L).
diff -r 0b8e87bb91d9 -r fb4186e20148 src/HOL/BCV/DFAimpl.thy
--- a/src/HOL/BCV/DFAimpl.thy	Fri Jul 07 17:15:17 2000 +0200
+++ b/src/HOL/BCV/DFAimpl.thy	Fri Jul 07 18:27:47 2000 +0200
@@ -34,11 +34,11 @@
  step_pres_type :: "(nat => 's => 's option) => nat => 's set => bool"
 "step_pres_type step n L == !s:L. !p<n. !t. step p s = Some(t) --> t:L"
 
- step_mono_None :: "(nat => 's => 's option) => nat => 's set => bool"
+ step_mono_None :: "(nat => 's::ord => 's option) => nat => 's set => bool"
 "step_mono_None step n L == !s p t.
    s : L & p < n & s <= t & step p s = None --> step p t = None"
 
- step_mono :: "(nat => 's => 's option) => nat => 's set => bool"
+ step_mono :: "(nat => 's::ord => 's option) => nat => 's set => bool"
 "step_mono step n L == !s p t u.
    s : L & p < n & s <= t & step p s = Some(u)
    --> (!v. step p t = Some(v) --> u <= v)"
diff -r 0b8e87bb91d9 -r fb4186e20148 src/HOL/Real/Hyperreal/Zorn.thy
--- a/src/HOL/Real/Hyperreal/Zorn.thy	Fri Jul 07 17:15:17 2000 +0200
+++ b/src/HOL/Real/Hyperreal/Zorn.thy	Fri Jul 07 18:27:47 2000 +0200
@@ -5,24 +5,24 @@
     Description : Zorn's Lemma -- See lcp's Zorn.thy in ZF
 *) 
 
-Zorn = Main +  
+Zorn = Main +
 
 constdefs
-  chain     ::  'a set => 'a set set
+  chain     ::  'a::ord set => 'a set set
     "chain S  == {F. F <= S & (ALL x: F. ALL y: F. x <= y | y <= x)}" 
 
-  super     ::  ['a set,'a set] => (('a set) set) 
+  super     ::  ['a::ord set,'a set] => 'a set set
     "super S c == {d. d: chain(S) & c < d}"
 
-  maxchain  ::  'a set => 'a set set
+  maxchain  ::  'a::ord set => 'a set set
     "maxchain S == {c. c: chain S & super S c = {}}"
 
-  succ      ::  ['a set,'a set] => 'a set
+  succ      ::  ['a::ord set,'a set] => 'a set
     "succ S c == if (c ~: chain S| c: maxchain S) 
                  then c else (@c'. c': (super S c))" 
 
 consts 
-  "TFin" :: 'a set => 'a set set
+  "TFin" :: 'a::ord set => 'a set set
 
 inductive "TFin(S)"
   intrs
diff -r 0b8e87bb91d9 -r fb4186e20148 src/HOL/Real/Lubs.thy
--- a/src/HOL/Real/Lubs.thy	Fri Jul 07 17:15:17 2000 +0200
+++ b/src/HOL/Real/Lubs.thy	Fri Jul 07 18:27:47 2000 +0200
@@ -11,20 +11,20 @@
 
 consts
     
-    "*<=" :: ['a set, 'a] => bool     (infixl 70)
-    "<=*" :: ['a, 'a set] => bool     (infixl 70)
+    "*<=" :: ['a set, 'a::ord] => bool     (infixl 70)
+    "<=*" :: ['a::ord, 'a set] => bool     (infixl 70)
 
 constdefs
-    leastP      :: ['a =>bool,'a] => bool
+    leastP      :: ['a =>bool,'a::ord] => bool
     "leastP P x == (P x & x <=* Collect P)"
 
-    isLub       :: ['a set, 'a set, 'a] => bool    
+    isLub       :: ['a set, 'a set, 'a::ord] => bool    
     "isLub R S x  == leastP (isUb R S) x"
 
-    isUb        :: ['a set, 'a set, 'a] => bool     
+    isUb        :: ['a set, 'a set, 'a::ord] => bool     
     "isUb R S x   == S *<= x & x: R"
 
-    ubs         :: ['a set, 'a set] => 'a set
+    ubs         :: ['a set, 'a::ord set] => 'a set
     "ubs R S      == Collect (isUb R S)"
 
 defs
diff -r 0b8e87bb91d9 -r fb4186e20148 src/HOL/ex/LocaleGroup.thy
--- a/src/HOL/ex/LocaleGroup.thy	Fri Jul 07 17:15:17 2000 +0200
+++ b/src/HOL/ex/LocaleGroup.thy	Fri Jul 07 18:27:47 2000 +0200
@@ -14,7 +14,7 @@
   unit     :: "'a"
 
 constdefs
-  Group :: "('a, 'more) grouptype_scheme set"
+  Group :: "('a, 'more::more) grouptype_scheme set"
   "Group == {G. (bin_op G): carrier G -> carrier G -> carrier G &
 	        inverse G : carrier G -> carrier G 
              & unit G : carrier G &
diff -r 0b8e87bb91d9 -r fb4186e20148 src/HOL/ex/MonoidGroup.thy
--- a/src/HOL/ex/MonoidGroup.thy	Fri Jul 07 17:15:17 2000 +0200
+++ b/src/HOL/ex/MonoidGroup.thy	Fri Jul 07 18:27:47 2000 +0200
@@ -17,15 +17,15 @@
   inv :: "'a => 'a"
 
 constdefs
-  monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |) => bool"
+  monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more::more |) => bool"
   "monoid M == ALL x y z.
     times M (times M x y) z = times M x (times M y z) &
-    times M (one M) x & times M x (one M) = x"
+    times M (one M) x = x & times M x (one M) = x"
 
-  group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'more |) => bool"
+  group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'more::more |) => bool"
   "group G == monoid G & (ALL x. times G (inv G x) x = one G)"
 
-  reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |) =>
+  reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more::more |) =>
     (| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |)"
   "reverse M == M (| times := %x y. times M y x |)"