# HG changeset patch
# User wenzelm
# Date 877339539 -7200
# Node ID eb707467f8c5317869ed64cf5c13f9a6929e7b19
# Parent  34152864655cbeefffbd639a423a1a034e25ee4a
adapted to qualified names;

diff -r 34152864655c -r eb707467f8c5 src/HOL/Gfp.thy
--- 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
diff -r 34152864655c -r eb707467f8c5 src/HOL/HOL.thy
--- 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
 
diff -r 34152864655c -r eb707467f8c5 src/HOL/Lfp.thy
--- 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
diff -r 34152864655c -r eb707467f8c5 src/HOL/NatDef.thy
--- 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))))"
diff -r 34152864655c -r eb707467f8c5 src/HOL/Ord.thy
--- 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)"
diff -r 34152864655c -r eb707467f8c5 src/HOL/Prod.thy
--- 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"
 
diff -r 34152864655c -r eb707467f8c5 src/HOL/ROOT.ML
--- 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 *)
diff -r 34152864655c -r eb707467f8c5 src/HOL/Set.thy
--- 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 *)
diff -r 34152864655c -r eb707467f8c5 src/HOL/Sum.thy
--- 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)))"
diff -r 34152864655c -r eb707467f8c5 src/HOL/Univ.thy
--- 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)))"
diff -r 34152864655c -r eb707467f8c5 src/HOL/WF.thy
--- 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