# HG changeset patch
# User haftmann
# Date 1282066598 -7200
# Node ID 8f0cd11238a75907a802028bc398acaa3d24cb8f
# Parent  205e1d735bb1d82ffd7f4e3f9e84687286792293
deglobalization

diff -r 205e1d735bb1 -r 8f0cd11238a7 src/CCL/Set.thy
--- a/src/CCL/Set.thy	Tue Aug 17 17:57:19 2010 +0100
+++ b/src/CCL/Set.thy	Tue Aug 17 19:36:38 2010 +0200
@@ -4,8 +4,6 @@
 imports FOL
 begin
 
-global
-
 typedecl 'a set
 arities set :: ("term") "term"
 
@@ -46,8 +44,6 @@
   "ALL x:A. P"  == "CONST Ball(A, %x. P)"
   "EX x:A. P"   == "CONST Bex(A, %x. P)"
 
-local
-
 axioms
   mem_Collect_iff:       "(a : {x. P(x)}) <-> P(a)"
   set_extension:         "A=B <-> (ALL x. x:A <-> x:B)"
diff -r 205e1d735bb1 -r 8f0cd11238a7 src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Tue Aug 17 17:57:19 2010 +0100
+++ b/src/Sequents/LK0.thy	Tue Aug 17 19:36:38 2010 +0200
@@ -12,8 +12,6 @@
 imports Sequents
 begin
 
-global
-
 classes "term"
 default_sort "term"
 
@@ -61,8 +59,6 @@
   Ex  (binder "\<exists>" 10) and
   not_equal  (infixl "\<noteq>" 50)
 
-local
-
 axioms
 
   (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
diff -r 205e1d735bb1 -r 8f0cd11238a7 src/Sequents/Sequents.thy
--- a/src/Sequents/Sequents.thy	Tue Aug 17 17:57:19 2010 +0100
+++ b/src/Sequents/Sequents.thy	Tue Aug 17 19:36:38 2010 +0200
@@ -14,8 +14,6 @@
 
 declare [[unify_trace_bound = 20, unify_search_bound = 40]]
 
-global
-
 typedecl o
 
 (* Sequences *)