changeset 61385 | 538100cc4399 |
parent 60770 | 240563fbf41d |
child 61386 | 0a29a984a91b |
--- a/src/Sequents/Sequents.thy Sat Oct 10 19:22:05 2015 +0200 +++ b/src/Sequents/Sequents.thy Sat Oct 10 20:51:39 2015 +0200 @@ -19,9 +19,7 @@ subsection \<open>Sequences\<close> -typedecl - seq' - +typedecl seq' consts SeqO' :: "[o,seq']=>seq'" Seq1' :: "o=>seq'" @@ -149,4 +147,3 @@ ML_file "prover.ML" end -