--- a/src/Pure/pure_syn.ML Sat Oct 17 20:27:12 2015 +0200
+++ b/src/Pure/pure_syn.ML Sat Oct 17 21:15:10 2015 +0200
@@ -34,6 +34,14 @@
(Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
val _ =
+ Outer_Syntax.command ("paragraph", @{here}) "paragraph heading"
+ (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
+
+val _ =
+ Outer_Syntax.command ("subparagraph", @{here}) "subparagraph heading"
+ (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
+
+val _ =
Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
(Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});