--- 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)"
--- 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).
--- 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)"
--- 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
--- 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
--- 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 &
--- 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 |)"