diff --git a/AssertLong.thy b/AssertLong.thy index a029ec6..dceefba 100644 --- a/AssertLong.thy +++ b/AssertLong.thy @@ -7,7 +7,7 @@ begin -ML{* +ML\ fun value_maybe_select some_name = case some_name @@ -30,11 +30,11 @@ fun value_cmd2 some_name modes raw_t state = Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); in Pretty.writeln p end; -*} -ML{* value_cmd2*} +\ +ML\value_cmd2\ definition ASSERT :: "bool \ bool" where "ASSERT p == (p=True)" -ML{* val x = @{code "ASSERT"} *} -ML{* +ML\val x = @{code "ASSERT"}\ +ML\ val opt_modes = Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []; @@ -49,9 +49,9 @@ val _ = (* Toplevel.keep (Value_Command.value_cmd some_name modes (enclose "ASSERT(" ")" t)) *) Toplevel.keep (value_cmd2 some_name modes t) end)); -*} +\ assert "True" assert "True \ True " -ML{* !TT ; - @{term "True"} *} \ No newline at end of file +ML\!TT ; + @{term "True"}\ \ No newline at end of file diff --git a/Isa_DOF.thy b/Isa_DOF.thy index ae925ac..f503469 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -731,7 +731,7 @@ typedecl "thm" typedecl "file" typedecl "thy" -\ \ and others in the future : file, http, thy, ... \ +\ \and others in the future : file, http, thy, ...\ consts ISA_typ :: "string \ typ" ("@{typ _}") consts ISA_term :: "string \ term" ("@{term _}") diff --git a/RegExp.thy b/RegExp.thy index 5d663f2..781c323 100644 --- a/RegExp.thy +++ b/RegExp.thy @@ -25,22 +25,22 @@ definition opt :: "'a rexp \ 'a rexp" ("\(_)\") where "\A\ \ A || One" value "Star (Conc(Alt (Atom(CHR ''a'')) (Atom(CHR ''b''))) (Atom(CHR ''c'')))" -text{* or better equivalently: *} +text\or better equivalently:\ value "\(\CHR ''a''\ || \CHR ''b''\) ~~ \CHR ''c''\\\<^sup>*" -section{* Definition of a semantic function: the ``language'' of the regular expression *} +section\Definition of a semantic function: the ``language'' of the regular expression\ text\ This is just a reminder - already defined in @{theory Regular_Exp} as @{term lang}.\ -text{* In the following, we give a semantics for our regular expressions, which so far have +text\In the following, we give a semantics for our regular expressions, which so far have just been a term language (i.e. abstract syntax). The semantics is a ``denotational semantics'', i.e. we give a direct meaning for regular expressions in some universe of ``denotations''. -This universe of denotations is in our concrete case: *} +This universe of denotations is in our concrete case:\ definition enabled :: "('a,'\ set)da \ '\ set \ 'a list \ 'a list" where "enabled A \ = filter (\x. next A x \ \ {}) " -text{* Now the denotational semantics for regular expression can be defined on a post-card: *} +text\Now the denotational semantics for regular expression can be defined on a post-card:\ fun L :: "'a rexp => 'a lang" where L_Emp : "L Zero = {}" diff --git a/RegExpInterface.thy b/RegExpInterface.thy index 24f65a4..c3f795d 100644 --- a/RegExpInterface.thy +++ b/RegExpInterface.thy @@ -37,20 +37,20 @@ definition opt :: "'a rexp \ 'a rexp" ("\(_)\") where "\A\ \ A || One" value "Star (Conc(Alt (Atom(CHR ''a'')) (Atom(CHR ''b''))) (Atom(CHR ''c'')))" -text{* or better equivalently: *} +text\or better equivalently:\ value "\(\CHR ''a''\ || \CHR ''b''\) ~~ \CHR ''c''\\\<^sup>*" -section{* Some Standard and Derived Semantics *} +section\Some Standard and Derived Semantics\ text\ This is just a reminder - already defined in @{theory "Regular-Sets.Regular_Exp"} as @{term lang}.\ -text{* In the following, we give a semantics for our regular expressions, which so far have +text\In the following, we give a semantics for our regular expressions, which so far have just been a term language (i.e. abstract syntax). The semantics is a ``denotational semantics'', i.e. we give a direct meaning for regular expressions in some universe of ``denotations''. -This universe of denotations is in our concrete case: *} +This universe of denotations is in our concrete case:\ -text{* Now the denotational semantics for regular expression can be defined on a post-card: *} +text\Now the denotational semantics for regular expression can be defined on a post-card:\ fun L :: "'a rexp => 'a lang" where L_Emp : "L Zero = {}" diff --git a/examples/math_exam/MathExam/MathExam.thy b/examples/math_exam/MathExam/MathExam.thy index a29ed2e..6ec6eef 100644 --- a/examples/math_exam/MathExam/MathExam.thy +++ b/examples/math_exam/MathExam/MathExam.thy @@ -8,18 +8,18 @@ open_monitor*[exam::MathExam] section*[header::Header,examSubject= "[algebra]", - date="''02-05-2018''", timeAllowed="90::int"] {* Exam number 1 *} -text{* + date="''02-05-2018''", timeAllowed="90::int"] \Exam number 1\ +text\ \begin{itemize} \item Use black ink or black ball-point pen. \item Draw diagrams in pencil. \item Answer all questions in the spaces provided. \end{itemize} -*} +\ text*[idir::Author, affiliation="''CentraleSupelec''", email="''idir.aitsadoune@centralesupelec.fr''"] - {*Idir AIT SADOUNE*} + \Idir AIT SADOUNE\ figure*[figure::figure, spawn_columns=False, @@ -29,7 +29,7 @@ figure*[figure::figure, spawn_columns=False, subsubsection*[exo1 :: Exercise, content="[q1::Task,q2::Task]"]\Exercise 1\ -text{* +text\ Here are the first four lines of a number pattern. \begin{itemize} \item Line 1 : @{term "1*6 + 2*4 = 2*7"} @@ -37,15 +37,15 @@ Here are the first four lines of a number pattern. \item Line 3 : @{term "3*8 + 2*6 = 4*9"} \item Line 4 : @{term "4*9 + 2*7 = 5*10"} \end{itemize} -*} +\ declare [[show_sorts=false]] subsubsection*[exo2 :: Exercise, content="[q1::Task,q2::Task]"]\Exercise 2\ -text{* Find the roots of the polynome: +text\Find the roots of the polynome: @{term "(x^3) - 6 * x^2 + 5 * x + 12"}. -Note the intermediate steps in the following fields and submit the solution. *} -text{* +Note the intermediate steps in the following fields and submit the solution.\ +text\ \begin{Form}[action={http://your-web-server.com/path/receiveform.cgi}] \begin{tabular}{l} From @{term "(x^3) - 6 * x^2 + 5 * x + 12"} \\\\ @@ -57,7 +57,7 @@ text{* \Submit{Submit}\\ \end{tabular} \end{Form} -*} +\ (* a bit brutal, as long as lemma* does not yet work *) (*<*) @@ -79,20 +79,20 @@ proof - qed (*>*) -text*[a1::Answer_Formal_Step]{* First Step: Fill in term and justification *} -text*[a2::Answer_Formal_Step]{* Next Step: Fill in term and justification *} -text*[a3::Answer_Formal_Step]{* Next Step: Fill in term and justification *} -text*[a4::Answer_Formal_Step]{* Next Step: Fill in term and justification *} +text*[a1::Answer_Formal_Step]\First Step: Fill in term and justification\ +text*[a2::Answer_Formal_Step]\Next Step: Fill in term and justification\ +text*[a3::Answer_Formal_Step]\Next Step: Fill in term and justification\ +text*[a4::Answer_Formal_Step]\Next Step: Fill in term and justification\ text*[q1::Task, local_grade="oneStar", mark="1::int", type="formal"] -{* Complete Line 10 : @{term "10*x + 2*y = 11*16"} *} +\Complete Line 10 : @{term "10*x + 2*y = 11*16"}\ subsubsection*[exo3 :: Exercise, content="[q1::Task,q2::Task]"]\Exercise 3\ text*[q2::Task, local_grade="threeStars", mark="3::int", type="formal"] -{* Prove that @{term "n*(n+5) + 2*(n+3) "} is always the product of two numbers +\Prove that @{term "n*(n+5) + 2*(n+3) "} is always the product of two numbers with a difference of 5. -*} +\ (* this does not work on the level of the LaTeX output for known restrictions of the Toplevel. *) close_monitor*[exam :: MathExam] diff --git a/examples/technical_report/IsaDof_Manual/04_IsaDofImpl.thy b/examples/technical_report/IsaDof_Manual/04_IsaDofImpl.thy index 1aacde8..4176d9e 100644 --- a/examples/technical_report/IsaDof_Manual/04_IsaDofImpl.thy +++ b/examples/technical_report/IsaDof_Manual/04_IsaDofImpl.thy @@ -26,7 +26,7 @@ is based on several design-decisions: \ -subsection*["sec:plugins"::technical]{*Writing \isadof as User-Defined Plugin in Isabelle/Isar*} +subsection*["sec:plugins"::technical]\Writing \isadof as User-Defined Plugin in Isabelle/Isar\ text\ Writing an own plugin in Isabelle starts with defining the local data and registering it in the framework. As mentioned before, contexts @@ -142,7 +142,7 @@ front-end supporting PIDE, a popup window with the text: ``declare document reference'' will appear. \ -subsection*["sec:prog_anti"::technical]{*Programming Text Antiquotations*} +subsection*["sec:prog_anti"::technical]\Programming Text Antiquotations\ text\ As mentioned in the introduction, Isabelle/Isar is configured with a number of standard commands to annotate formal definitions and proofs diff --git a/examples/technical_report/IsaDof_Manual/05_DesignImpl.thy b/examples/technical_report/IsaDof_Manual/05_DesignImpl.thy index c183f4c..e679ac4 100644 --- a/examples/technical_report/IsaDof_Manual/05_DesignImpl.thy +++ b/examples/technical_report/IsaDof_Manual/05_DesignImpl.thy @@ -5,7 +5,7 @@ begin (*>*) chapter*[impl2::technical,main_author="Some(@{docitem ''bu''}::author)"] - {* \isadof: Design and Implementation*} + \\isadof: Design and Implementation\ text\ In this section, we present the design and implementation of \isadof. \subsection{Document Ontology Modeling with \isadof} @@ -110,7 +110,7 @@ expression consisting of the class identifier \inlineisar+A+, \inlineisar+B+, etc. Its use is discussed in \autoref{sec:monitor-class}. \ -subsection*[editing::example]{*Editing a Document with Ontology-Conform Meta-Data*} +subsection*[editing::example]\Editing a Document with Ontology-Conform Meta-Data\ text\ As already mentioned, Isabelle/Isar comes with a number of standard \emph{text commands} such as \inlineisar+section{* ... *}+ or @@ -193,7 +193,7 @@ referencing it, although the actual text-element will occur later in the document.\ -subsection*[ontolinks::technical]{*Ontology-Conform Logical Links: \isadof Antiquotations*} +subsection*[ontolinks::technical]\Ontology-Conform Logical Links: \isadof Antiquotations\ text\ Up to this point, the world of the formal and the informal document parts are strictly separated. The main objective of \isadof are ways @@ -305,7 +305,7 @@ enforce that terms or theorems have a particular form or correspond to ``claims'' (contributions) listed in the introduction of the paper. \ -subsection*["sec:monitor-class"::technical]{*Monitor Document Classes*} +subsection*["sec:monitor-class"::technical]\Monitor Document Classes\ text\ \autoref{lst:example} shows our conceptual running example in all details. While inheritance on document classes allows for structuring @@ -353,7 +353,7 @@ text\ \end{isar} \ -section{*Document Generation*} +section\Document Generation\ text\ Up to know, we discussed the definition of ontologies and their representation in an interactive development environment, \ie, diff --git a/ontologies/CENELEC_50128.thy b/ontologies/CENELEC_50128.thy index a732fb1..80cc32c 100644 --- a/ontologies/CENELEC_50128.thy +++ b/ontologies/CENELEC_50128.thy @@ -388,7 +388,7 @@ doc_class TC = requirement + section\Software Assurance related Entities and Concepts\ -text{* subcategories are : *} +text\subcategories are :\ text\Table A.13: \ diff --git a/ontologies/mathex_onto.thy b/ontologies/mathex_onto.thy index 7ec139c..5e71341 100644 --- a/ontologies/mathex_onto.thy +++ b/ontologies/mathex_onto.thy @@ -3,7 +3,7 @@ theory mathex_onto begin (*<<*) -text{* In our scenario, content has four different types of addressees: +text\In our scenario, content has four different types of addressees: \<^item> the @{emph \setter\}, i.e. the author of the exam, \<^item> the @{emph \student\}, i.e. the addressee of the exam, \<^item> the @{emph \checker\}, i.e. a person that checks the exam for @@ -13,7 +13,7 @@ text{* In our scenario, content has four different types of addressees: Note that the latter quality assurance mechanism is used in many universities, where for organizational reasons the execution of an exam takes place in facilities where the author of the exam is not expected to be physically present. -*} +\ datatype ContentClass = @@ -76,12 +76,12 @@ doc_class Exercise = Exam_item + concerns :: "ContentClass set" <= "{setter,student,checker,externalExaminer}" -text{* In many institutions, it makes sense to have a rigorous process of validation +text\In many institutions, it makes sense to have a rigorous process of validation for exam subjects : is the initial question correct ? Is a proof in the sense of the question possible ? We model the possibility that the @{term setter} validates a question by a sample proof validated by Isabelle. In our scenario this sample proofs are completely @{emph \intern\}, i.e. not exposed to the students but just additional -material for the internal review process of the exam.*} +material for the internal review process of the exam.\ doc_class Validation = tests :: "term list" <="[]" diff --git a/ontologies/scholarly_paper.thy b/ontologies/scholarly_paper.thy index 58e4062..a46dae1 100644 --- a/ontologies/scholarly_paper.thy +++ b/ontologies/scholarly_paper.thy @@ -1,4 +1,4 @@ -section{* An example ontology for a scholarly paper*} +section\An example ontology for a scholarly paper\ theory scholarly_paper imports "../Isa_COL" @@ -45,7 +45,7 @@ doc_class technical = text_section + definition_list :: "string list" <= "[]" formal_results :: "thm list" -text{* A very rough formatting style could be modeled as follows:*} +text\A very rough formatting style could be modeled as follows:\ doc_class example = text_section + diff --git a/ontologies/small_math.thy b/ontologies/small_math.thy index 0859676..a0aefe5 100644 --- a/ontologies/small_math.thy +++ b/ontologies/small_math.thy @@ -1,4 +1,4 @@ -section{* An example ontology for a math paper*} +section\An example ontology for a math paper\ theory small_math imports "../Isa_COL" diff --git a/ontologies/technical_report.thy b/ontologies/technical_report.thy index 79a54b8..48b9929 100644 --- a/ontologies/technical_report.thy +++ b/ontologies/technical_report.thy @@ -1,4 +1,4 @@ -section{* An example ontology for a scholarly paper*} +section\An example ontology for a scholarly paper\ theory technical_report imports "scholarly_paper"