# HG changeset patch # User wenzelm # Date 1178732240 -7200 # Node ID adc529c89281e3c971b5ff8d90c6e57873648cd2 # Parent 619b270607ac098fd69277375c6e54efd72853f2 tuned syntax; diff -r 619b270607ac -r adc529c89281 src/Sequents/ILL_predlog.thy --- a/src/Sequents/ILL_predlog.thy Wed May 09 19:37:19 2007 +0200 +++ b/src/Sequents/ILL_predlog.thy Wed May 09 19:37:20 2007 +0200 @@ -11,11 +11,13 @@ disj :: "[plf,plf] => plf" (infixr "|" 35) impl :: "[plf,plf] => plf" (infixr ">" 35) eq :: "[plf,plf] => plf" (infixr "=" 35) - "@NG" :: "plf => plf" ("- _ " [50] 55) ff :: "plf" PL :: "plf => o" ("[* / _ / *]" [] 100) +syntax + "_NG" :: "plf => plf" ("- _ " [50] 55) + translations "[* A & B *]" == "[*A*] && [*B*]"