src/Tools/isac/BaseDefinitions/Know_Store.thy
changeset 60509 2e0b7ca391dc
parent 60508 ce09935439b3
child 60521 23c40bb1bdbf
     1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Aug 03 18:17:27 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Thu Aug 04 12:48:37 2022 +0200
     1.3 @@ -68,8 +68,8 @@
     1.4  *)
     1.5  signature KESTORE_ELEMS =
     1.6  sig
     1.7 -  val get_rew_ord: theory -> Rewrite_Ord.rew_ord list
     1.8 -  val add_rew_ord: Rewrite_Ord.rew_ord list -> theory -> theory
     1.9 +  val get_rew_ord: theory -> Rewrite_Ord.T list
    1.10 +  val add_rew_ord: Rewrite_Ord.T list -> theory -> theory
    1.11    val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
    1.12    val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
    1.13    val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list