diff --git a/examples/cenelec/mini_odo/mini_odo.thy b/examples/cenelec/mini_odo/mini_odo.thy index 12dd136..d442de8 100644 --- a/examples/cenelec/mini_odo/mini_odo.thy +++ b/examples/cenelec/mini_odo/mini_odo.thy @@ -70,9 +70,11 @@ section*[h::example]\ Some global inspection commands for the status of do section*[i::example]\ Text Antiquotation Infrastructure ... \ - + +(*<*) text\ @{docitem \lalala\} -- produces warning. \ text\ @{docitem (unchecked) \lalala\} -- produces no warning. \ +(*>*) text\ @{docitem \ass122\} -- global reference to a text-item in another file. \