equal
deleted
inserted
replaced
84 val get_expls: theory -> Example.store |
84 val get_expls: theory -> Example.store |
85 val add_expls: (Example.T * Store.key) list -> theory -> theory |
85 val add_expls: (Example.T * Store.key) list -> theory -> theory |
86 val get_ref_last_thy: unit -> theory |
86 val get_ref_last_thy: unit -> theory |
87 val set_ref_last_thy: theory -> unit |
87 val set_ref_last_thy: theory -> unit |
88 val get_via_last_thy: ThyC.id -> theory (*only used for * (Sub-)problem retrieving respective thy |
88 val get_via_last_thy: ThyC.id -> theory (*only used for * (Sub-)problem retrieving respective thy |
89 * problem refinement *) |
89 * problem refinement |
|
90 * (test-)code to be deleted *) |
90 end; |
91 end; |
91 |
92 |
92 structure Know_Store(**): KNOW_STORE(**) = |
93 structure Know_Store(**): KNOW_STORE(**) = |
93 struct |
94 struct |
94 structure Data = Theory_Data ( |
95 structure Data = Theory_Data ( |