diff -r 0fd80c27fdf5 -r f270e3e18be5 src/Sequents/Sequents.thy
--- a/src/Sequents/Sequents.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/Sequents/Sequents.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -40,17 +40,15 @@
  "_SeqO"           :: "o => seqobj"                        ("_")
  "_SeqId"          :: "'a => seqobj"                       ("$_")
 
-types
- single_seqe = "[seq,seqobj] => prop"
- single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
- two_seqi    = "[seq'=>seq', seq'=>seq'] => prop"
- two_seqe    = "[seq, seq] => prop"
- three_seqi  = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
- three_seqe  = "[seq, seq, seq] => prop"
- four_seqi   = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
- four_seqe   = "[seq, seq, seq, seq] => prop"
-
- sequence_name = "seq'=>seq'"
+type_synonym single_seqe = "[seq,seqobj] => prop"
+type_synonym single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
+type_synonym two_seqi = "[seq'=>seq', seq'=>seq'] => prop"
+type_synonym two_seqe = "[seq, seq] => prop"
+type_synonym three_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
+type_synonym three_seqe = "[seq, seq, seq] => prop"
+type_synonym four_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
+type_synonym four_seqe = "[seq, seq, seq, seq] => prop"
+type_synonym sequence_name = "seq'=>seq'"
 
 
 syntax