theory COL_Test imports "Isabelle_DOF_Unit_Tests_document" begin print_doc_items print_doc_classes section\General Heading COL Elements\ chapter*[S1::"chapter"]\Chapter\ text*[S1'::"chapter"]\Chapter\ section*[S2::"section"]\Section\ text*[S2'::"section"]\Section\ subsection*[S3::"subsection"]\Subsection\ text*[S3'::"subsection"]\Subsection\ subsubsection*[S4::"subsubsection"]\Subsubsection\ text*[S4'::"subsubsection"]\Subsubsection\ paragraph*[S5::"paragraph"]\PAragraph\ text*[S5'::"paragraph"]\Paragraph\ section\General Figure COL Elements\ figure*[fig1_test,relative_width="95",file_src="''figures/A.png''"] \ This is the label text \<^term>\\\<^sub>i+2\ \ (*<*) (* text* with type figure not supported *) text*[fig2_test::figure, relative_width="95",file_src="''figures/A.png''" ]\ This is the label text\ text\check @{figure fig1_test} cmp to @{figure fig2_test}\ (*>*) (* And a side-chick ... *) text*[inlinefig::float, main_caption="\The Caption.\"] \@{theory_text [display, margin = 5] \lemma A :: "a \ b"\}\ text*[dupl_graphics::float, main_caption="\The Caption.\"] \ @{fig_content (width=40, height=35, caption="This is a left test") "figures/A.png" }\<^hfill>@{fig_content (width=40, height=35, caption="This is a right \<^term>\\\<^sub>i + 1\ test") "figures/B.png"} \ end (*>*)