From aff78b062507eab0d88a87f1b133a03af597c5e8 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 26 Mar 2022 19:31:23 +0000 Subject: [PATCH] Restructuring. --- NOTES.thy => src/tests/Isabelle2021-1.thy | 8 ++------ src/tests/ROOT | 1 + 2 files changed, 3 insertions(+), 6 deletions(-) rename NOTES.thy => src/tests/Isabelle2021-1.thy (96%) 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 737fb3d..bec44b9 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 4ef831b..d9a69c2 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"