--- 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)"
--- 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] *)
--- 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 *)