forked from Isabelle_DOF/Isabelle_DOF
Restructuring.
This commit is contained in:
parent
9f5d20a586
commit
aff78b0625
|
@ -1,6 +1,6 @@
|
||||||
chapter \<open>Notes on Isabelle/DOF for Isabelle2021-1\<close>
|
chapter \<open>Notes on Isabelle/DOF for Isabelle2021-1\<close>
|
||||||
|
|
||||||
theory NOTES
|
theory "Isabelle2021-1"
|
||||||
imports Main
|
imports Main
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
@ -16,10 +16,6 @@ text \<open>
|
||||||
|
|
||||||
\<^verbatim>\<open>isabelle components -l\<close>
|
\<^verbatim>\<open>isabelle components -l\<close>
|
||||||
|
|
||||||
\<^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>\<open>datatype\<close> or \<^verbatim>\<open>structure\<close> in ML).
|
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
|
@ -7,5 +7,6 @@ session "Isabelle_DOF-tests" = "Isabelle_DOF" +
|
||||||
"TermAntiquotations"
|
"TermAntiquotations"
|
||||||
"Attributes"
|
"Attributes"
|
||||||
"Evaluation"
|
"Evaluation"
|
||||||
|
"Isabelle2021-1"
|
||||||
"High_Level_Syntax_Invariants"
|
"High_Level_Syntax_Invariants"
|
||||||
"Ontology_Matching_Example"
|
"Ontology_Matching_Example"
|
||||||
|
|
Loading…
Reference in New Issue