forked from Isabelle_DOF/Isabelle_DOF
Base examples on the session Isabelle_DOF.
This commit is contained in:
parent
97fc51a8ae
commit
b91377edbd
|
@ -1,5 +1,5 @@
|
||||||
theory BAC2017
|
theory BAC2017
|
||||||
imports "../../../ontologies/mathex_onto"
|
imports "Isabelle_DOF.mathex_onto"
|
||||||
Deriv
|
Deriv
|
||||||
Transcendental
|
Transcendental
|
||||||
begin
|
begin
|
||||||
|
|
|
@ -1,7 +1,6 @@
|
||||||
session "BAC2017" = "Functional-Automata" +
|
session "BAC2017" = "Isabelle_DOF" +
|
||||||
options [document = pdf, document_output = "output",quick_and_dirty=true]
|
options [document = pdf, document_output = "output",quick_and_dirty=true]
|
||||||
theories [document = false]
|
theories [document = false]
|
||||||
"../../../ontologies/mathex_onto"
|
|
||||||
"Deriv"
|
"Deriv"
|
||||||
"Transcendental"
|
"Transcendental"
|
||||||
theories
|
theories
|
||||||
|
|
|
@ -1,6 +1,6 @@
|
||||||
(*<*)
|
(*<*)
|
||||||
theory MathExam
|
theory MathExam
|
||||||
imports "../../../ontologies/mathex_onto"
|
imports "Isabelle_DOF.mathex_onto"
|
||||||
Real
|
Real
|
||||||
begin
|
begin
|
||||||
(*>*)
|
(*>*)
|
||||||
|
|
|
@ -1,8 +1,5 @@
|
||||||
session "MathExam" = "Functional-Automata" +
|
session "MathExam" = "Isabelle_DOF" +
|
||||||
options [document = pdf, document_output = "output"]
|
options [document = pdf, document_output = "output"]
|
||||||
theories [document = false]
|
|
||||||
(* Foo *)
|
|
||||||
"../../../ontologies/mathex_onto"
|
|
||||||
theories
|
theories
|
||||||
MathExam
|
MathExam
|
||||||
document_files
|
document_files
|
||||||
|
|
|
@ -1,6 +1,6 @@
|
||||||
(*<*)
|
(*<*)
|
||||||
theory IsaDofApplications
|
theory IsaDofApplications
|
||||||
imports "../../../ontologies/scholarly_paper"
|
imports "Isabelle_DOF.scholarly_paper"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
open_monitor*[this::article]
|
open_monitor*[this::article]
|
||||||
|
|
|
@ -1,7 +1,5 @@
|
||||||
session "IsaDofApplications" = "Functional-Automata" +
|
session "IsaDofApplications" = "Isabelle_DOF" +
|
||||||
options [document = pdf, document_output = "output", quick_and_dirty = true]
|
options [document = pdf, document_output = "output", quick_and_dirty = true]
|
||||||
theories [document = false]
|
|
||||||
"../../../ontologies/scholarly_paper"
|
|
||||||
theories
|
theories
|
||||||
IsaDofApplications
|
IsaDofApplications
|
||||||
document_files
|
document_files
|
||||||
|
|
|
@ -1,6 +1,6 @@
|
||||||
(*<*)
|
(*<*)
|
||||||
theory "00_Frontmatter"
|
theory "00_Frontmatter"
|
||||||
imports "../../../ontologies/technical_report"
|
imports "Isabelle_DOF.technical_report"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
open_monitor*[this::report]
|
open_monitor*[this::report]
|
||||||
|
|
|
@ -1,8 +1,5 @@
|
||||||
session "IsaDof_Manual" = "Functional-Automata" +
|
session "IsaDof_Manual" = "Isabelle_DOF" +
|
||||||
options [document = pdf, document_output = "output", quick_and_dirty = true]
|
options [document = pdf, document_output = "output", quick_and_dirty = true]
|
||||||
theories [document = false]
|
|
||||||
"../../../ontologies/scholarly_paper"
|
|
||||||
"../../../ontologies/technical_report"
|
|
||||||
theories
|
theories
|
||||||
IsaDofManual
|
IsaDofManual
|
||||||
document_files
|
document_files
|
||||||
|
|
|
@ -1,6 +1,6 @@
|
||||||
(*<*)
|
(*<*)
|
||||||
theory MyCommentedIsabelle
|
theory MyCommentedIsabelle
|
||||||
imports "../../../ontologies/technical_report"
|
imports "Isabelle_DOF.technical_report"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -1,8 +1,5 @@
|
||||||
session "TR_mycommentedisabelle" = "Functional-Automata" +
|
session "TR_mycommentedisabelle" = "Isabelle_DOF" +
|
||||||
options [document = pdf, document_output = "output",quick_and_dirty = true]
|
options [document = pdf, document_output = "output",quick_and_dirty = true]
|
||||||
theories [document = false]
|
|
||||||
"../../../ontologies/scholarly_paper"
|
|
||||||
"../../../ontologies/technical_report"
|
|
||||||
theories
|
theories
|
||||||
"MyCommentedIsabelle"
|
"MyCommentedIsabelle"
|
||||||
document_files
|
document_files
|
||||||
|
|
Loading…
Reference in New Issue