Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Removed local debugging hacks that break proper build.

This commit is contained in:
Achim D. Brucker 2019-06-17 10:07:21 +01:00
parent f53d43afd2
commit 8a8fac042e
1 changed files with 2 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
examples/cenelec/mini_odo/mini_odo.thy
View File

@ -1,11 +1,7 @@
theory mini_odo
(*
imports "Isabelle_DOF.CENELEC_50128"
"Isabelle_DOF.scholarly_paper"
*)
imports "../../../ontologies/CENELEC_50128"
"../../../ontologies/scholarly_paper"
begin
@ -32,13 +28,13 @@ text\<open>An "anonymous" text-item, automatically coerced into the top-class "t
text*[tralala] \<open> Brexit means Brexit \<close>
text\<open>Examples for declaration of typed doc-items "assumption" and "hypothesis",
concepts defined in the underlying ontology @{theory "Draft.CENELEC_50128"}. \<close>
concepts defined in the underlying ontology @{theory "Isabelle_DOF.CENELEC_50128"}. \<close>
text*[ass1::assumption] \<open> The subsystem Y is safe. \<close>
text*[hyp1::hypothesis] \<open> P not equal NP \<close>
text\<open>A real example fragment from a larger project, declaring a text-element as a
"safety-related application condition", a concept defined in the
@{theory "Draft.CENELEC_50128"} ontology:\<close>
@{theory "Isabelle_DOF.CENELEC_50128"} ontology:\<close>
text*[new_ass::hypothesis]\<open>Under the assumption @{assumption \<open>ass1\<close>} we establish the following: ... \<close>