diff --git a/NOTES.thy b/src/tests/Isabelle2021-1.thy similarity index 96% rename from NOTES.thy rename to src/tests/Isabelle2021-1.thy index 737fb3d2..bec44b9c 100644 --- a/NOTES.thy +++ b/src/tests/Isabelle2021-1.thy @@ -1,6 +1,6 @@ chapter \Notes on Isabelle/DOF for Isabelle2021-1\ -theory NOTES +theory "Isabelle2021-1" imports Main begin @@ -16,10 +16,6 @@ text \ \<^verbatim>\isabelle components -l\ - \<^item> In the private terminology of Burkhart, the word "component" has a - different meaning: a tool implemented in Isabelle/ML that happens to - declare context data (many ML tools do that, it is not very special, - similar to defining a \<^verbatim>\datatype\ or \<^verbatim>\structure\ in ML). \ @@ -252,4 +248,4 @@ ML \ end -(* :maxLineLen=75: *) \ No newline at end of file +(* :maxLineLen=75: *) diff --git a/src/tests/ROOT b/src/tests/ROOT index 4ef831b9..d9a69c26 100755 --- a/src/tests/ROOT +++ b/src/tests/ROOT @@ -7,5 +7,6 @@ session "Isabelle_DOF-tests" = "Isabelle_DOF" + "TermAntiquotations" "Attributes" "Evaluation" + "Isabelle2021-1" "High_Level_Syntax_Invariants" "Ontology_Matching_Example"