From bce097b1d6d7ce2db9949d544a8a97dcc332b12b Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Mon, 15 May 2023 13:02:41 +0200 Subject: [PATCH] Commenting out refs to definitionSTAR --- Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy b/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy index 6175fc0..31aa9af 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy @@ -108,13 +108,15 @@ find_theorems name:tagged "(_::cc_assumption_test \ _ \ declare_reference-assert-error[c1::C]\Duplicate instance declaration\ \ \forward declaration\ declare_reference*[e6::E] - +(*<*) (* pdf GENERATION NEEDS TO BE IMPLEMENTED IN FRONT AND BACKEND *) text\This is the answer to the "OutOfOrder Presentation Problem": @{E (unchecked) \e6\} \ definition*[e6::E] facu :: "nat \ nat" where "facu arg = undefined" text\As shown in @{E \e5\} following from @{E \e6\}\ + +(*>*) text\As shown in @{C \c4\}\