--- a/src/Sequents/Sequents.thy Sat Feb 01 00:32:32 2014 +0000
+++ b/src/Sequents/Sequents.thy Sat Feb 01 17:56:03 2014 +0100
@@ -7,6 +7,7 @@
theory Sequents
imports Pure
+keywords "print_pack" :: diag
begin
setup Pure_Thy.old_appl_syntax_setup
@@ -15,7 +16,8 @@
typedecl o
-(* Sequences *)
+
+subsection {* Sequences *}
typedecl
seq'
@@ -25,7 +27,7 @@
Seq1' :: "o=>seq'"
-(* concrete syntax *)
+subsection {* Concrete syntax *}
nonterminal seq and seqobj and seqcont
@@ -141,6 +143,9 @@
parse_translation {* [(@{syntax_const "_Side"}, K side_tr)] *}
+
+subsection {* Proof tools *}
+
ML_file "prover.ML"
end