diff -r 5d8a9900cabc -r bafb24c150c1 src/Sequents/S43.thy --- a/src/Sequents/S43.thy Wed May 19 11:41:58 2004 +0200 +++ b/src/Sequents/S43.thy Fri May 21 21:14:18 2004 +0200 @@ -11,6 +11,7 @@ consts S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop" +syntax "@S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop" ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)