Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Sequents/LK0.thy
changeset 35417 47ee18b6ae32
parent 35355 613e133966ea
parent 35416 d8d7d1b785af
child 36452 d37c6eed8117 
--- a/src/Sequents/LK0.thy	Mon Mar 01 12:30:55 2010 +0100
+++ b/src/Sequents/LK0.thy	Mon Mar 01 13:42:31 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)"
isabelle