Merge branch 'master' into Unreleased/Isabelle2018
Isabelle_DOF/Isabelle_DOF/Unreleased%2FIsabelle2018 This commit looks good
Details
Isabelle_DOF/Isabelle_DOF/Unreleased%2FIsabelle2018 This commit looks good
Details
This commit is contained in:
commit
2341879f06
|
@ -55,7 +55,7 @@ in your \inlinebash|PATH|, you will need to invoke \inlinebash|isabelle| using i
|
||||||
full qualified path, \eg:
|
full qualified path, \eg:
|
||||||
|
|
||||||
\begin{bash}
|
\begin{bash}
|
||||||
ë\prompt{}ë /usr/local/Isabelleë\isabelleversionë/bin/isabelle version
|
ë\prompt{}ë /usr/local/Isabelleë\isabelleversion/ëbin/isabelle version
|
||||||
ë\isabellefullversionë
|
ë\isabellefullversionë
|
||||||
\end{bash}
|
\end{bash}
|
||||||
\<close>
|
\<close>
|
||||||
|
@ -75,11 +75,9 @@ text\<open>
|
||||||
|
|
||||||
\begin{bash}
|
\begin{bash}
|
||||||
ë\prompt{}ë pdftex \\expanded{Success}\\end
|
ë\prompt{}ë pdftex \\expanded{Success}\\end
|
||||||
This is pdfTeX, Version 3.14159265-2.6-1.40.20 (TeX Live 2019/Debian) (preloaded format=pdftex)
|
This is pdfTeX, Version 3.14159265-2.6-1.40.20 (TeX Live 2019/Debian).
|
||||||
restricted \write18 enabled.
|
|
||||||
entering extended mode
|
entering extended mode
|
||||||
[1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}]</usr/share/texlive/texmf
|
[1{dftex.map}]<cmr10.pfb>
|
||||||
-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb>
|
|
||||||
Output written on texput.pdf (1 page, 8650 bytes).
|
Output written on texput.pdf (1 page, 8650 bytes).
|
||||||
Transcript written on texput.log.
|
Transcript written on texput.log.
|
||||||
\end{bash}
|
\end{bash}
|
||||||
|
@ -113,6 +111,7 @@ If the \inlinebash|isabelle| tool is not in your \inlinebash|PATH|, you need to
|
||||||
\inlinebash|install| script with the \inlinebash|--isabelle| option, passing the full-qualified
|
\inlinebash|install| script with the \inlinebash|--isabelle| option, passing the full-qualified
|
||||||
path of the \inlinebash|isabelle| tool (\inlinebash|install --help| gives
|
path of the \inlinebash|isabelle| tool (\inlinebash|install --help| gives
|
||||||
you an overview of all available configuration options):
|
you an overview of all available configuration options):
|
||||||
|
\clearpage
|
||||||
|
|
||||||
\begin{bash}
|
\begin{bash}
|
||||||
ë\prompt{}ë cd ë\isadofdirnë
|
ë\prompt{}ë cd ë\isadofdirnë
|
||||||
|
|
|
@ -215,7 +215,8 @@ text\<open>
|
||||||
with the syntactic category of \<open>name\<close>'s we refer to alpha-numerical identifiers
|
with the syntactic category of \<open>name\<close>'s we refer to alpha-numerical identifiers
|
||||||
(called \<open>short_id\<close>'s in @{cite "wenzel:isabelle-isar:2019"}) and identifiers
|
(called \<open>short_id\<close>'s in @{cite "wenzel:isabelle-isar:2019"}) and identifiers
|
||||||
in \inlineisar+" ... "+ which might contain certain ``quasi-letters'' such
|
in \inlineisar+" ... "+ which might contain certain ``quasi-letters'' such
|
||||||
as \inlineisar+_+, \inlineisar+-+, \inlineisar+.+. See~@{cite "wenzel:isabelle-isar:2019"} for details.
|
as \inlineisar+_+, \inlineisar+-+, \inlineisar+.+ (see~@{cite "wenzel:isabelle-isar:2019"} for
|
||||||
|
details).
|
||||||
\<^item> \<open>tyargs\<close>:\index{tyargs@\<open>tyargs\<close>}
|
\<^item> \<open>tyargs\<close>:\index{tyargs@\<open>tyargs\<close>}
|
||||||
\<^rail>\<open> typefree | ('(' (typefree * ',') ')')\<close>
|
\<^rail>\<open> typefree | ('(' (typefree * ',') ')')\<close>
|
||||||
\<open>typefree\<close> denotes fixed type variable(\<open>'a\<close>, \<open>'b\<close>, ...) (see~@{cite "wenzel:isabelle-isar:2019"})
|
\<open>typefree\<close> denotes fixed type variable(\<open>'a\<close>, \<open>'b\<close>, ...) (see~@{cite "wenzel:isabelle-isar:2019"})
|
||||||
|
@ -280,6 +281,7 @@ A document class\bindex{document class} can be defined using the @{command "doc_
|
||||||
\<^rail>\<open> 'rejects' (class_id * ',') \<close>
|
\<^rail>\<open> 'rejects' (class_id * ',') \<close>
|
||||||
\<^item> \<open>default_clause\<close>:\index{default\_clause@\<open>default_clause\<close>}
|
\<^item> \<open>default_clause\<close>:\index{default\_clause@\<open>default_clause\<close>}
|
||||||
\<^rail>\<open> '<=' '"' expr '"' \<close>
|
\<^rail>\<open> '<=' '"' expr '"' \<close>
|
||||||
|
\clearpage
|
||||||
\<^item> \<open>regexpr\<close>:\index{regexpr@\<open>regexpr\<close>}
|
\<^item> \<open>regexpr\<close>:\index{regexpr@\<open>regexpr\<close>}
|
||||||
\<^rail>\<open> '\<lfloor>' class_id '\<rfloor>' | '(' regexpr ')' | (regexpr '||' regexpr) | (regexpr '~~' regexpr)
|
\<^rail>\<open> '\<lfloor>' class_id '\<rfloor>' | '(' regexpr ')' | (regexpr '||' regexpr) | (regexpr '~~' regexpr)
|
||||||
| ('\<lbrace>' regexpr '\<rbrace>') | ( '\<lbrace>' regexpr '\<rbrace>\<^sup>*') \<close>
|
| ('\<lbrace>' regexpr '\<rbrace>') | ( '\<lbrace>' regexpr '\<rbrace>\<^sup>*') \<close>
|
||||||
|
@ -380,7 +382,7 @@ doc_class EC = AC +
|
||||||
representation. Note that the \inlineltx|\newisadof{}[]{}|-command requires the
|
representation. Note that the \inlineltx|\newisadof{}[]{}|-command requires the
|
||||||
full-qualified names, \eg, \inlineisar|t$$ext.CENELEC_50128.EC| for the document class and
|
full-qualified names, \eg, \inlineisar|t$$ext.CENELEC_50128.EC| for the document class and
|
||||||
\inlineisar|CENELEC_50128.requirement.long_name| for the attribute \inlineisar|long_name|,
|
\inlineisar|CENELEC_50128.requirement.long_name| for the attribute \inlineisar|long_name|,
|
||||||
inherited from the document class \inlineisar|requirement|. The document representation of ECs
|
inherited from the document class \inlineisar|requirement|. The representation of ECs
|
||||||
can now be defined as follows:
|
can now be defined as follows:
|
||||||
|
|
||||||
\begin{ltx}
|
\begin{ltx}
|
||||||
|
@ -415,12 +417,11 @@ doc_class EC = AC +
|
||||||
|
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
(*<*)
|
||||||
text*[aaa::assertions]\<open>description with validations I and II\<close>
|
text*[aaa::assertions]\<open>description with validations I and II\<close>
|
||||||
assert*[aaa::assertions] "3 < (4::int)"
|
assert*[aaa::assertions] "3 < (4::int)"
|
||||||
assert*[aaa::assertions] "0 < (4::int)"
|
assert*[aaa::assertions] "0 < (4::int)"
|
||||||
|
(*>*)
|
||||||
|
|
||||||
|
|
||||||
subsection*["text-elements"::technical]\<open>Annotatable Top-level Text-Elements\<close>
|
subsection*["text-elements"::technical]\<open>Annotatable Top-level Text-Elements\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
|
@ -433,8 +434,7 @@ text\<open>
|
||||||
title*[title::title]\<Open>Isabelle/DOF\<Close>
|
title*[title::title]\<Open>Isabelle/DOF\<Close>
|
||||||
subtitle*[subtitle::subtitle]\<Open>User and Implementation Manual\<Close>
|
subtitle*[subtitle::subtitle]\<Open>User and Implementation Manual\<Close>
|
||||||
text*[adb:: author, email="\<Open>a.brucker@exeter.ac.uk\<Close>",
|
text*[adb:: author, email="\<Open>a.brucker@exeter.ac.uk\<Close>",
|
||||||
orcid="\<Open>0000-0002-6355-1200\<Close>",
|
orcid="\<Open>0000-0002-6355-1200\<Close>", http_site="\<Open>https://brucker.ch/\<Close>",
|
||||||
http_site="\<Open>https://brucker.ch/\<Close>",
|
|
||||||
affiliation="\<Open>University of Exeter, Exeter, UK\<Close>"] \<Open>Achim D. Brucker\<Close>
|
affiliation="\<Open>University of Exeter, Exeter, UK\<Close>"] \<Open>Achim D. Brucker\<Close>
|
||||||
text*[bu::author, email = "\<Open>wolff@lri.fr\<Close>",
|
text*[bu::author, email = "\<Open>wolff@lri.fr\<Close>",
|
||||||
affiliation = "\<Open>Université Paris-Saclay, LRI, Paris, France\<Close>"]\<Open>Burkhart Wolff\<Close>
|
affiliation = "\<Open>Université Paris-Saclay, LRI, Paris, France\<Close>"]\<Open>Burkhart Wolff\<Close>
|
||||||
|
@ -447,7 +447,11 @@ text\<open>
|
||||||
that has an identity as a text-object labelled as \<open>obj_id\<close>, belongs to a document class
|
that has an identity as a text-object labelled as \<open>obj_id\<close>, belongs to a document class
|
||||||
\<open>class_id\<close> that has been defined earlier, and has its class-attributes set with particular
|
\<open>class_id\<close> that has been defined earlier, and has its class-attributes set with particular
|
||||||
values (which are denotable in Isabelle/HOL mathematical term syntax).
|
values (which are denotable in Isabelle/HOL mathematical term syntax).
|
||||||
|
\<^item> \<open>meta_args\<close> :
|
||||||
|
\<^rail>\<open>(obj_id ('::' class_id) ((attribute '=' term)) * ',')\<close>
|
||||||
|
\<^item> \<open>rich_meta_args\<close> :
|
||||||
|
\<^rail>\<open> (obj_id ('::' class_id) ((attribute (('=' | '+=') term)) * ','))\<close>
|
||||||
|
\clearpage
|
||||||
\<^item> \<open>annotated_text_element\<close> :
|
\<^item> \<open>annotated_text_element\<close> :
|
||||||
\<^rail>\<open>
|
\<^rail>\<open>
|
||||||
( ( @@{command "title*"}
|
( ( @@{command "title*"}
|
||||||
|
@ -466,11 +470,6 @@ text\<open>
|
||||||
| change_status_command
|
| change_status_command
|
||||||
| inspection_command
|
| inspection_command
|
||||||
\<close>
|
\<close>
|
||||||
\clearpage
|
|
||||||
\<^item> \<open>meta_args\<close> :
|
|
||||||
\<^rail>\<open>(obj_id ('::' class_id) ((attribute '=' term)) * ',')\<close>
|
|
||||||
\<^item> \<open>rich_meta_args\<close> :
|
|
||||||
\<^rail>\<open> (obj_id ('::' class_id) ((attribute (('=' | '+=') term)) * ','))\<close>
|
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue