src/HOL/Set.thy
changeset 3947 eb707467f8c5
parent 3842 b55686a7b22c
child 4151 5c19cd418c33
--- 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 *)