Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Cleanup.

This commit is contained in:
Achim D. Brucker 2021-01-07 04:39:28 +00:00
parent 225309482b
commit 82121d7204
1 changed files with 5 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy
View File

@ -1,7 +1,7 @@
(************************************************************************* (*************************************************************************
* Copyright (C) * Copyright (C)
* 2019-2020 The University of Exeter * 2019-2021 The University of Exeter
* 2018-2020 The University of Paris-Saclay * 2018-2021 The University of Paris-Saclay
* 2018 The University of Sheffield * 2018 The University of Sheffield
* *
* License: * License:
@ -88,24 +88,16 @@ text\<open>
\<^item> a light-blue background for input written in Isabelle's Isar language, \<^eg>: \<^item> a light-blue background for input written in Isabelle's Isar language, \<^eg>:
@{boxed_theory_text [display] @{boxed_theory_text [display]
\<open>lemma refl: "x = x" \<open>lemma refl: "x = x"
by simp\<close>} by simp\<close>}
\<^item> a green background for examples of generated document fragments (\<^ie>, PDF output): \<^item> a green background for examples of generated document fragments (\<^ie>, PDF output):
@{boxed_pdf [display] \<open>The axiom refl\<close>} @{boxed_pdf [display] \<open>The axiom refl\<close>}
\<^item> a red background for For (S)ML-code: \<^item> a red background for For (S)ML-code:
@{boxed_sml [display] \<open>fun id x = x\<close>} @{boxed_sml [display] \<open>fun id x = x\<close>}
\<^item> a yellow background for \LaTeX-code: \<^item> a yellow background for \LaTeX-code:
@{boxed_latex [display] \<open>\newcommand{\refl}{$x = x$}\<close>} @{boxed_latex [display] \<open>\newcommand{\refl}{$x = x$}\<close>}
\begin{ltx}
\newcommand{\refl}{$x = x$}
\end{ltx}
\<^item> a grey background for shell scripts and interactive shell sessions: \<^item> a grey background for shell scripts and interactive shell sessions:
@{boxed_bash [display] @{boxed_bash [display]\<open>ë\prompt{}ë ls
\<open>ë\prompt{}ë ls CHANGELOG.md CITATION examples install LICENSE README.md ROOTS src\<close>}
CHANGELOG.md CITATION examples install LICENSE README.md ROOTS src\<close>}
\begin{bash}
ë\prompt{}ë ls
CHANGELOG.md CITATION examples install LICENSE README.md ROOTS src
\end{bash}
\<close> \<close>
subsubsection\<open>How to Cite \<^isadof>\<close> subsubsection\<open>How to Cite \<^isadof>\<close>