Updated license information.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
This commit is contained in:
parent
6cd8cb098b
commit
60ebbbe12c
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
theory
|
theory
|
||||||
mini_odo
|
mini_odo
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
theory MathExam
|
theory MathExam
|
||||||
imports "Isabelle_DOF.math_exam"
|
imports "Isabelle_DOF.math_exam"
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
theory IsaDofApplications
|
theory IsaDofApplications
|
||||||
imports "Isabelle_DOF.scholarly_paper"
|
imports "Isabelle_DOF.scholarly_paper"
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
theory "00_Frontmatter"
|
theory "00_Frontmatter"
|
||||||
imports "Isabelle_DOF.technical_report"
|
imports "Isabelle_DOF.technical_report"
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
theory "01_Introduction"
|
theory "01_Introduction"
|
||||||
imports "00_Frontmatter"
|
imports "00_Frontmatter"
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
theory "02_Background"
|
theory "02_Background"
|
||||||
imports "01_Introduction"
|
imports "01_Introduction"
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
theory
|
theory
|
||||||
"03_GuidedTour"
|
"03_GuidedTour"
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
theory
|
theory
|
||||||
"04_RefMan"
|
"04_RefMan"
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
theory "05_Implementation"
|
theory "05_Implementation"
|
||||||
imports "04_RefMan"
|
imports "04_RefMan"
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
theory "Isabelle_DOF-Manual"
|
theory "Isabelle_DOF-Manual"
|
||||||
imports "05_Implementation"
|
imports "05_Implementation"
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
theory TR_MyCommentedIsabelle
|
theory TR_MyCommentedIsabelle
|
||||||
imports "Isabelle_DOF.technical_report"
|
imports "Isabelle_DOF.technical_report"
|
||||||
|
@ -2108,4 +2121,4 @@ close_monitor*[this]
|
||||||
check_doc_global
|
check_doc_global
|
||||||
|
|
||||||
end
|
end
|
||||||
(*>*)
|
(*>*)
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
section \<open> Little theory implementing the an assertion command in Isabelle/HOL. \<close>
|
section \<open> Little theory implementing the an assertion command in Isabelle/HOL. \<close>
|
||||||
text\<open>This command is useful for certification documents allowing to validate
|
text\<open>This command is useful for certification documents allowing to validate
|
||||||
corner-cases of (executable) definitions. \<close>
|
corner-cases of (executable) definitions. \<close>
|
||||||
|
@ -66,4 +79,4 @@ assert "True \<and> True "
|
||||||
assert "(5::int) * 5 = 25 "
|
assert "(5::int) * 5 = 25 "
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
theory AssertLong
|
theory AssertLong
|
||||||
imports Main
|
imports Main
|
||||||
keywords "assert" ::thy_decl
|
keywords "assert" ::thy_decl
|
||||||
|
@ -54,4 +67,4 @@ val _ =
|
||||||
assert "True"
|
assert "True"
|
||||||
assert "True \<and> True "
|
assert "True \<and> True "
|
||||||
ML\<open>!TT ;
|
ML\<open>!TT ;
|
||||||
@{term "True"}\<close>
|
@{term "True"}\<close>
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
chapter \<open>The Document Ontology Common Library for the Isabelle Ontology Framework\<close>
|
chapter \<open>The Document Ontology Common Library for the Isabelle Ontology Framework\<close>
|
||||||
|
|
||||||
text\<open> Offering
|
text\<open> Offering
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
chapter \<open>The Document Ontology Framework for Isabelle\<close>
|
chapter \<open>The Document Ontology Framework for Isabelle\<close>
|
||||||
|
|
||||||
text\<open> Offering
|
text\<open> Offering
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
theory RegExp
|
theory RegExp
|
||||||
imports "Functional-Automata.Execute"
|
imports "Functional-Automata.Execute"
|
||||||
begin
|
begin
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
structure RegExpChecker : sig
|
structure RegExpChecker : sig
|
||||||
type 'a equal
|
type 'a equal
|
||||||
type num
|
type num
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
chapter\<open>The High-Level Interface to the Automata-Library\<close>
|
chapter\<open>The High-Level Interface to the Automata-Library\<close>
|
||||||
|
|
||||||
theory RegExpInterface
|
theory RegExpInterface
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
chapter \<open>An Outline of a CENELEC Ontology\<close>
|
chapter \<open>An Outline of a CENELEC Ontology\<close>
|
||||||
|
|
||||||
text\<open> NOTE: An Ontology-Model of a certification standard such as CENELEC or Common Criteria
|
text\<open> NOTE: An Ontology-Model of a certification standard such as CENELEC or Common Criteria
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
theory Conceptual
|
theory Conceptual
|
||||||
imports "../../DOF/Isa_DOF" "../../DOF/Isa_COL"
|
imports "../../DOF/Isa_DOF" "../../DOF/Isa_COL"
|
||||||
begin
|
begin
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
theory math_exam
|
theory math_exam
|
||||||
imports "../../DOF/Isa_COL"
|
imports "../../DOF/Isa_COL"
|
||||||
begin
|
begin
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
chapter \<open>The Document Ontology Common Library for the Isabelle Ontology Framework\<close>
|
chapter \<open>The Document Ontology Common Library for the Isabelle Ontology Framework\<close>
|
||||||
|
|
||||||
text\<open> Offering support for common Isabelle Elements like definitions, lemma- and theorem
|
text\<open> Offering support for common Isabelle Elements like definitions, lemma- and theorem
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
theory
|
theory
|
||||||
ontologies
|
ontologies
|
||||||
imports
|
imports
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
section\<open>An example ontology for a scholarly paper\<close>
|
section\<open>An example ontology for a scholarly paper\<close>
|
||||||
|
|
||||||
theory scholarly_paper
|
theory scholarly_paper
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
section\<open>An example ontology for a math paper\<close>
|
section\<open>An example ontology for a math paper\<close>
|
||||||
|
|
||||||
theory small_math
|
theory small_math
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
section\<open>An example ontology for a scholarly paper\<close>
|
section\<open>An example ontology for a scholarly paper\<close>
|
||||||
|
|
||||||
theory technical_report
|
theory technical_report
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
theory
|
theory
|
||||||
AssnsLemmaThmEtc
|
AssnsLemmaThmEtc
|
||||||
imports
|
imports
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
theory
|
theory
|
||||||
Attributes
|
Attributes
|
||||||
imports
|
imports
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
chapter\<open>Setting and modifying attributes of doc-items\<close>
|
chapter\<open>Setting and modifying attributes of doc-items\<close>
|
||||||
|
|
||||||
theory
|
theory
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
chapter\<open>Setting and modifying attributes of doc-items\<close>
|
chapter\<open>Setting and modifying attributes of doc-items\<close>
|
||||||
|
|
||||||
theory
|
theory
|
||||||
|
|
|
@ -1,3 +1,16 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* Copyright (C)
|
||||||
|
* 2019 The University of Exeter
|
||||||
|
* 2018-2019 The University of Paris-Saclay
|
||||||
|
* 2018 The University of Sheffield
|
||||||
|
*
|
||||||
|
* License:
|
||||||
|
* This program can be redistributed and/or modified under the terms
|
||||||
|
* of the 2-clause BSD-style license.
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
*************************************************************************)
|
||||||
|
|
||||||
chapter\<open>Inner Syntax Antiquotations (ISA)'s\<close>
|
chapter\<open>Inner Syntax Antiquotations (ISA)'s\<close>
|
||||||
|
|
||||||
theory
|
theory
|
||||||
|
|
Loading…
Reference in New Issue