2018-10-30 00:58:45 +00:00
|
|
|
(*<*)
|
2019-07-22 13:41:29 +00:00
|
|
|
theory "Isabelle_DOF-Manual"
|
2019-01-08 13:44:43 +00:00
|
|
|
imports "06_Conclusion"
|
2018-10-30 00:58:45 +00:00
|
|
|
begin
|
|
|
|
(*<*)
|
2018-12-04 05:31:45 +00:00
|
|
|
|
2019-07-17 17:08:59 +00:00
|
|
|
|
|
|
|
|
|
|
|
|
2019-01-08 13:44:43 +00:00
|
|
|
text*[bib::bibliography]\<open>References\<close>
|
2018-12-11 15:03:01 +00:00
|
|
|
|
2019-07-17 12:51:45 +00:00
|
|
|
(*<*)
|
|
|
|
|
2018-10-30 00:58:45 +00:00
|
|
|
close_monitor*[this]
|
|
|
|
|
2019-07-17 14:06:55 +00:00
|
|
|
check_doc_global
|
|
|
|
|
2018-10-30 00:58:45 +00:00
|
|
|
text\<open>Resulting trace in doc\_item ''this'': \<close>
|
|
|
|
ML\<open>@{trace_attribute this}\<close>
|
|
|
|
|
|
|
|
|
|
|
|
end
|
|
|
|
(*>*)
|
|
|
|
|