--- a/src/HOL/Gfp.thy Mon Oct 20 11:22:29 1997 +0200
+++ b/src/HOL/Gfp.thy Mon Oct 20 11:25:39 1997 +0200
@@ -8,8 +8,12 @@
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/HOL.thy Mon Oct 20 11:22:29 1997 +0200
+++ b/src/HOL/HOL.thy Mon Oct 20 11:25:39 1997 +0200
@@ -11,6 +11,8 @@
(** Core syntax **)
+global
+
classes
term < logic
@@ -33,6 +35,7 @@
Not :: bool => bool ("~ _" [40] 40)
True, False :: bool
If :: [bool, 'a, 'a] => 'a ("(if (_)/ then (_)/ else (_))" 10)
+ arbitrary :: 'a
(* Binders *)
@@ -141,6 +144,8 @@
(** Rules and definitions **)
+local
+
rules
eq_reflection "(x=y) ==> (x==y)"
@@ -179,9 +184,6 @@
o_def "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
if_def "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
-consts
- arbitrary :: 'a
-
end
--- a/src/HOL/Lfp.thy Mon Oct 20 11:22:29 1997 +0200
+++ b/src/HOL/Lfp.thy Mon Oct 20 11:25:39 1997 +0200
@@ -8,8 +8,12 @@
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/NatDef.thy Mon Oct 20 11:22:29 1997 +0200
+++ b/src/HOL/NatDef.thy Mon Oct 20 11:25:39 1997 +0200
@@ -12,6 +12,8 @@
(** type ind **)
+global
+
types
ind
@@ -59,6 +61,8 @@
"case p of 0 => a | Suc y => b" == "nat_case a (%y. b) p"
+local
+
defs
Zero_def "0 == Abs_Nat(Zero_Rep)"
Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
--- a/src/HOL/Ord.thy Mon Oct 20 11:22:29 1997 +0200
+++ b/src/HOL/Ord.thy Mon Oct 20 11:25:39 1997 +0200
@@ -11,6 +11,8 @@
axclass
ord < term
+global
+
syntax
"op <" :: ['a::ord, 'a] => bool ("op <")
"op <=" :: ['a::ord, 'a] => bool ("op <=")
@@ -28,6 +30,8 @@
"op <=" :: ['a::ord, 'a] => bool ("(_/ \\<le> _)" [50, 51] 50)
+local
+
defs
mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
min_def "min a b == (if a <= b then a else b)"
--- a/src/HOL/Prod.thy Mon Oct 20 11:22:29 1997 +0200
+++ b/src/HOL/Prod.thy Mon Oct 20 11:25:39 1997 +0200
@@ -18,6 +18,8 @@
Pair_Rep :: ['a, 'b] => ['a, 'b] => bool
"Pair_Rep == (%a b. %x y. x=a & y=b)"
+global
+
typedef (Prod)
('a, 'b) "*" (infixr 20)
= "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}"
@@ -71,6 +73,8 @@
(* definitions *)
+local
+
defs
Pair_def "Pair a b == Abs_Prod(Pair_Rep a b)"
fst_def "fst p == @a. ? b. p = (a, b)"
@@ -83,11 +87,15 @@
(** unit **)
+global
+
typedef unit = "{True}"
consts
"()" :: unit ("'(')")
+local
+
defs
Unity_def "() == Abs_unit True"
--- a/src/HOL/ROOT.ML Mon Oct 20 11:22:29 1997 +0200
+++ b/src/HOL/ROOT.ML Mon Oct 20 11:25:39 1997 +0200
@@ -7,9 +7,11 @@
Should be executed in the subdirectory HOL.
*)
-val banner = "Higher-Order Logic with curried functions";
+val banner = "Higher-Order Logic";
writeln banner;
+reset global_names;
+
print_depth 1;
(* Add user sections *)
--- a/src/HOL/Set.thy Mon Oct 20 11:22:29 1997 +0200
+++ b/src/HOL/Set.thy Mon Oct 20 11:25:39 1997 +0200
@@ -9,6 +9,8 @@
(** Core syntax **)
+global
+
types
'a set
@@ -121,6 +123,8 @@
(** Rules and definitions **)
+local
+
rules
(* Isomorphisms between Predicates and Sets *)
--- a/src/HOL/Sum.thy Mon Oct 20 11:22:29 1997 +0200
+++ b/src/HOL/Sum.thy Mon Oct 20 11:25:39 1997 +0200
@@ -17,6 +17,8 @@
Inr_Rep :: ['b, 'a, 'b, bool] => bool
"Inr_Rep == (%b. %x y p. y=b & ~p)"
+global
+
typedef (Sum)
('a, 'b) "+" (infixr 10)
= "{f. (? a. f = Inl_Rep(a::'a)) | (? b. f = Inr_Rep(b::'b))}"
@@ -36,6 +38,8 @@
translations
"case p of Inl x => a | Inr y => b" == "sum_case (%x. a) (%y. b) p"
+local
+
defs
Inl_def "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
Inr_def "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
--- a/src/HOL/Univ.thy Mon Oct 20 11:22:29 1997 +0200
+++ b/src/HOL/Univ.thy Mon Oct 20 11:25:39 1997 +0200
@@ -13,6 +13,8 @@
(** lists, trees will be sets of nodes **)
+global
+
typedef (Node)
'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}"
@@ -46,6 +48,9 @@
"<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set]
=> ('a item * 'a item)set" (infixr 70)
+
+local
+
defs
Push_Node_def "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
--- a/src/HOL/WF.thy Mon Oct 20 11:22:29 1997 +0200
+++ b/src/HOL/WF.thy Mon Oct 20 11:25:39 1997 +0200
@@ -8,6 +8,8 @@
WF = Trancl +
+global
+
constdefs
wf :: "('a * 'a)set => bool"
"wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
@@ -28,4 +30,6 @@
"wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
r x) x)"
+local
+
end