diff --git a/examples/CENELEC_50128/mini_odo/mini_odo.thy b/examples/CENELEC_50128/mini_odo/mini_odo.thy index 358f0e0..1db0044 100644 --- a/examples/CENELEC_50128/mini_odo/mini_odo.thy +++ b/examples/CENELEC_50128/mini_odo/mini_odo.thy @@ -615,8 +615,8 @@ text\ \<^item> \@{file "mini_odo.thy"}\ : @{file "mini_odo.thy"} \<^item> \@{value "3+4::int"}}\ : @{value "3+4::int"} \<^item> \@{const hd}\ : @{const hd} -\<^item> \@{theory HOL.List}\ : @{theory HOL.List} -\<^item> \@{term "3"}\ : @{term "3"} +\<^item> \@{theory HOL.List}\ : @{theory HOL.List}s +\<^item> \@{tserm "3"}\ : @{term "3"} \<^item> \@{type bool}\ : @{type bool} \<^item> \@{thm term [show_types] "f x = a + x"}\ : @{term [show_types] "f x = a + x"} \ @@ -624,10 +624,10 @@ text\ text\Examples for declaration of typed doc-classes "assumption" (sic!) and "hypothesis" (sic!!), concepts defined in the underlying ontology @{theory "Isabelle_DOF.CENELEC_50128"}. \ text*[ass2::assumption, long_name="Some ''assumption one''"] \ The subsystem Y is safe. \ -text*[hyp1::hypothesis] \ P not equal NP \ +text*[hyp1::hypothesis] \ P \ NP \ text\ - A real example fragment from a larger project, declaring a text-element as a + A real example fragment fsrom a larger project, declaring a text-element as a "safety-related application condition", a concept defined in the @{theory "Isabelle_DOF.CENELEC_50128"} ontology:\