From f437e1337cbc87c77128d1cb7a92820fcaf5132d Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 28 Apr 2018 17:41:34 +0100 Subject: [PATCH] Disable markdown. --- Isa_DOF.thy | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index da2569f..547f76f 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -499,17 +499,17 @@ val _ = val _ = Outer_Syntax.command ("paragraph*", @{here}) "paragraph heading" (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> enriched_document_command {markdown = true}); + >> enriched_document_command {markdown = false}); val _ = Outer_Syntax.command ("subparagraph*", @{here}) "subparagraph heading" (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> enriched_document_command {markdown = true}); + >> enriched_document_command {markdown = false}); val _ = Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)" (attributes -- Parse.opt_target -- Parse.document_source - >> enriched_document_command {markdown = true}); + >> enriched_document_command {markdown = false}); val _ = @@ -750,4 +750,4 @@ text {* Lq *} -end \ No newline at end of file +end