src/Sequents/LK0.thy
changeset 35416 d8d7d1b785af
parent 35113 1a0c129bb2e0
child 35417 47ee18b6ae32
--- a/src/Sequents/LK0.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/Sequents/LK0.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -122,8 +122,7 @@
   The: "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==>
           $H |- $E, P(THE x. P(x)), $F"
 
-constdefs
-  If :: "[o, 'a, 'a] => 'a"   ("(if (_)/ then (_)/ else (_))" 10)
+definition If :: "[o, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) where 
    "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"