src/Sequents/Sequents.thy
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
-