src/Sequents/LK0.thy

--- a/src/Sequents/LK0.thy	Tue Nov 21 00:00:39 2006 +0100
+++ b/src/Sequents/LK0.thy	Tue Nov 21 00:07:05 2006 +0100
@@ -129,9 +129,6 @@
   If :: "[o, 'a, 'a] => 'a"   ("(if (_)/ then (_)/ else (_))" 10)
    "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"
 
-setup
-  prover_setup
-
 
 (** Structural Rules on formulas **)
 
@@ -240,8 +237,6 @@
                             add_unsafes [thm "allL", thm "exR", thm "the_equality"];
 
 
-pack_ref() := LK_pack;
-
 local
   val thinR = thm "thinR"
   val thinL = thm "thinL"