src/Sequents/LK0.thy
changeset 16019 0e1405402d53
parent 14854 61bdf2ae4dc5
child 17481 75166ebb619b
--- a/src/Sequents/LK0.thy	Sun May 22 16:51:06 2005 +0200
+++ b/src/Sequents/LK0.thy	Sun May 22 16:51:07 2005 +0200
@@ -123,10 +123,6 @@
   If :: [o, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
    "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"
 
-
-setup
-  Simplifier.setup
-
 setup
   prover_setup