--- a/TFL/rules.sml Thu May 18 11:40:57 2000 +0200
+++ b/TFL/rules.sml Thu May 18 11:43:57 2000 +0200
@@ -427,7 +427,7 @@
let val {prop, ...} = rep_thm thm
in case prop
of (Const("==>",_)$(Const("Trueprop",_)$ _) $
- (Const("==",_) $ (Const ("cut",_) $ f $ R $ a $ x) $ _)) => false
+ (Const("==",_) $ (Const ("WF.cut",_) $ f $ R $ a $ x) $ _)) => false
| _ => true
end;
@@ -631,7 +631,7 @@
end;
fun restricted t = is_some (S.find_term
- (fn (Const("cut",_)) =>true | _ => false)
+ (fn (Const("WF.cut",_)) =>true | _ => false)
t)
fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
--- a/TFL/usyntax.sml Thu May 18 11:40:57 2000 +0200
+++ b/TFL/usyntax.sml Thu May 18 11:43:57 2000 +0200
@@ -321,7 +321,7 @@
mesg="unexpected term structure"}
else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"};
-fun is_WFR (Const("wf",_)$_) = true
+fun is_WFR (Const("WF.wf",_)$_) = true
| is_WFR _ = false;
fun ARB ty = mk_select{Bvar=Free("v",ty),
--- a/src/HOL/Gfp.thy Thu May 18 11:40:57 2000 +0200
+++ b/src/HOL/Gfp.thy Thu May 18 11:43:57 2000 +0200
@@ -8,12 +8,8 @@
Gfp = Lfp +
-global
-
constdefs
gfp :: ['a set=>'a set] => 'a set
"gfp(f) == Union({u. u <= f(u)})" (*greatest fixed point*)
-local
-
end
--- a/src/HOL/Lfp.thy Thu May 18 11:40:57 2000 +0200
+++ b/src/HOL/Lfp.thy Thu May 18 11:43:57 2000 +0200
@@ -8,12 +8,8 @@
Lfp = mono + Prod +
-global
-
constdefs
lfp :: ['a set=>'a set] => 'a set
"lfp(f) == Inter({u. f(u) <= u})" (*least fixed point*)
-local
-
end
--- a/src/HOL/Ord.thy Thu May 18 11:40:57 2000 +0200
+++ b/src/HOL/Ord.thy Thu May 18 11:43:57 2000 +0200
@@ -12,26 +12,26 @@
axclass
ord < term
-global
-
syntax
"op <" :: ['a::ord, 'a] => bool ("op <")
"op <=" :: ['a::ord, 'a] => bool ("op <=")
+global
+
consts
"op <" :: ['a::ord, 'a] => bool ("(_/ < _)" [50, 51] 50)
"op <=" :: ['a::ord, 'a] => bool ("(_/ <= _)" [50, 51] 50)
- mono :: ['a::ord => 'b::ord] => bool (*monotonicity*)
- min, max :: ['a::ord, 'a] => 'a
- Least :: ('a::ord=>bool) => 'a (binder "LEAST " 10)
+local
syntax (symbols)
"op <=" :: ['a::ord, 'a] => bool ("op \\<le>")
"op <=" :: ['a::ord, 'a] => bool ("(_/ \\<le> _)" [50, 51] 50)
-
-local
+consts
+ mono :: ['a::ord => 'b::ord] => bool (*monotonicity*)
+ min, max :: ['a::ord, 'a] => 'a
+ Least :: ('a::ord=>bool) => 'a (binder "LEAST " 10)
defs
mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
--- a/src/HOL/WF.thy Thu May 18 11:40:57 2000 +0200
+++ b/src/HOL/WF.thy Thu May 18 11:43:57 2000 +0200
@@ -8,8 +8,6 @@
WF = Trancl +
-global
-
constdefs
wf :: "('a * 'a)set => bool"
"wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
@@ -30,6 +28,4 @@
"wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
r x) x)"
-local
-
end