changeset 62453 | b93cc7d73431 |
parent 61464 | d35ff80f27fb |
child 62876 | 507c90523113 |
--- a/src/Pure/pure_syn.ML Sun Feb 28 15:57:03 2016 +0100 +++ b/src/Pure/pure_syn.ML Sun Feb 28 17:37:20 2016 +0100 @@ -14,10 +14,6 @@ struct val _ = - Outer_Syntax.command ("header", @{here}) "theory header" - (Parse.document_source >> Thy_Output.old_header_command); - -val _ = Outer_Syntax.command ("chapter", @{here}) "chapter heading" (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});