diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index fd2e4ce..99489e9 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -559,6 +559,9 @@ text\ where "(title ~~ \subtitle\ ~~ \author\$^+$+ ~~ abstract ~~ introduction ~~ \technical || example\$^+$ ~~ conclusion ~~ bibliography)" + % TODO: + % Update to the new implementation. + % where is deprecated and the new implementation uses accepts and rejects. \} In a integrated document source, the body of the content can be paranthesized into: @@ -664,6 +667,10 @@ doc_class requirement = long_name :: "string option" doc_class requirement_analysis = no :: "nat" where "requirement_item +" +% TODO: +% Update to the new implementation. +% where is deprecated and the new implementation uses accepts and rejects. + doc_class hypothesis = requirement + hyp_type :: hyp_type <= physical (* default *) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 6a1ef8c..22caaf3 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -114,6 +114,9 @@ text\ \<^emph>\is-a\ relation between classes; \<^item> classes may refer to other classes via a regular expression in a \<^emph>\where\ clause; + % TODO: + % Update to the new implementation. + % where is deprecated and the new implementation uses accepts and rejects. \<^item> attributes may have default values in order to facilitate notation. \ @@ -146,6 +149,9 @@ text\ classes and their inheritance relation structure meta-data of text-elements in an object-oriented manner, monitor classes enforce structural organization of documents via the language specified by the regular expression enforcing a sequence of text-elements. + % TODO: + % Update to the new implementation. + % where is deprecated and the new implementation uses accepts and rejects. A major design decision of ODL is to denote attribute values by HOL-terms and HOL-types. Consequently, ODL can refer to any predefined type defined in the HOL library, \<^eg>,