src/Pure/pure_syn.ML
changeset 61463 8e46cea6a45a
parent 61457 3e21699bb83b
child 61464 d35ff80f27fb
--- 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});