From aa1fed24403514d77dfc106df9a22e9e0cd85078 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Mon, 2 Nov 2020 14:12:27 +0100 Subject: [PATCH] sdf --- src/DOF/Isa_COL.thy | 6 ++---- src/ontologies/scholarly_paper/scholarly_paper.thy | 4 ++++ 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index 7211fab..07c7622 100755 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -398,10 +398,8 @@ section\Tables\ section\Tests\ ML\@{term "side_by_side_figure"}; -@{typ "doc_class rexp"}; -DOF_core.SPY; -\ - + @{typ "doc_class rexp"}; + DOF_core.SPY;\ section\DEPRECATED : An attempt to model Standard Isabelle Formal Content\ diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 287ed47..8c9668a 100755 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -420,6 +420,10 @@ fun check_group a = map (check_group_elem (check_level_hd (hd a))) (tl a) ; section\Miscelleous\ +ML\ +Parse.int +\ + subsection\Layout Trimming Commands\ setup\ DOF_lib.define_macro \<^binding>\hs\ "\\hspace{" "}" (K(K())) \ setup\ DOF_lib.define_macro \<^binding>\vs\ "\\vspace{" "}" (K(K())) \