pierre.derathe
/
Isabelle_DOF
Archived
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Removed obsolete "extend" operation

This commit is contained in:
Makarius Wenzel 2022-12-02 15:31:23 +01:00
parent bb5963c6e2
commit a6c1a2baa4
3 changed files with 1 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy
View File

@ -53,7 +53,6 @@ text\<open>
\<open>structure Data = Generic_Data \<open>structure Data = Generic_Data
( type T = docobj_tab * docclass_tab * ... ( type T = docobj_tab * docclass_tab * ...
val empty = (initial_docobj_tab, initial_docclass_tab, ...) val empty = (initial_docobj_tab, initial_docclass_tab, ...)
val extend = I
fun merge((d1,c1,...),(d2,c2,...)) = (merge_docobj_tab (d1,d2,...), fun merge((d1,c1,...),(d2,c2,...)) = (merge_docobj_tab (d1,d2,...),
merge_docclass_tab(c1,c2,...)) merge_docclass_tab(c1,c2,...))
);\<close>} );\<close>}

4
examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
View File

@ -364,7 +364,7 @@ subsection*[t213::example]\<open>Mechanism 2 : Extending the Global Context \<op
text\<open>A central mechanism for constructing user-defined data is by the \<^ML_functor>\<open>Generic_Data\<close>-functor. text\<open>A central mechanism for constructing user-defined data is by the \<^ML_functor>\<open>Generic_Data\<close>-functor.
A plugin needing some data \<^verbatim>\<open>T\<close> and providing it with implementations for an A plugin needing some data \<^verbatim>\<open>T\<close> and providing it with implementations for an
\<^verbatim>\<open>empty\<close>, and operations \<^verbatim>\<open>merge\<close> and \<^verbatim>\<open>extend\<close>, can construct a lense with operations \<^verbatim>\<open>empty\<close>, and operation \<^verbatim>\<open>merge\<close>, can construct a lense with operations
\<^verbatim>\<open>get\<close> and \<^verbatim>\<open>put\<close> that attach this data into the generic system context. Rather than using \<^verbatim>\<open>get\<close> and \<^verbatim>\<open>put\<close> that attach this data into the generic system context. Rather than using
unsynchronized SML mutable variables, this is the mechanism to introduce component local unsynchronized SML mutable variables, this is the mechanism to introduce component local
data in Isabelle, which allows to manage this data for the necessary backtrack and synchronization data in Isabelle, which allows to manage this data for the necessary backtrack and synchronization
@ -373,14 +373,12 @@ text\<open>A central mechanism for constructing user-defined data is by the \<^M
ML \<open> ML \<open>
datatype X = mt datatype X = mt
val init = mt; val init = mt;
val ext = I
fun merge (X,Y) = mt fun merge (X,Y) = mt
structure Data = Generic_Data structure Data = Generic_Data
( (
type T = X type T = X
val empty = init val empty = init
val extend = ext
val merge = merge val merge = merge
); );
\<close> \<close>

1
src/DOF/Isa_DOF.thy
View File

@ -251,7 +251,6 @@ structure Data = Generic_Data
docclass_eager_inv_tab = initial_docclass_eager_inv_tab, docclass_eager_inv_tab = initial_docclass_eager_inv_tab,
docclass_lazy_inv_tab = initial_docclass_lazy_inv_tab docclass_lazy_inv_tab = initial_docclass_lazy_inv_tab
} }
val extend = I
fun merge( {docobj_tab=d1,docclass_tab = c1, fun merge( {docobj_tab=d1,docclass_tab = c1,
ISA_transformer_tab = e1, monitor_tab=m1, ISA_transformer_tab = e1, monitor_tab=m1,
docclass_inv_tab = n1, docclass_inv_tab = n1,