equal
deleted
inserted
replaced
66 |
66 |
67 get_* retrieves all * of the respective theory PLUS of all ancestor theories. |
67 get_* retrieves all * of the respective theory PLUS of all ancestor theories. |
68 *) |
68 *) |
69 signature KESTORE_ELEMS = |
69 signature KESTORE_ELEMS = |
70 sig |
70 sig |
71 val get_rew_ord: theory -> Rewrite_Ord.rew_ord list |
71 val get_rew_ord: theory -> Rewrite_Ord.T list |
72 val add_rew_ord: Rewrite_Ord.rew_ord list -> theory -> theory |
72 val add_rew_ord: Rewrite_Ord.T list -> theory -> theory |
73 val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list |
73 val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list |
74 val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory |
74 val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory |
75 val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list |
75 val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list |
76 val add_calcs: (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list -> theory -> theory |
76 val add_calcs: (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list -> theory -> theory |
77 val get_cas: theory -> CAS_Def.T list |
77 val get_cas: theory -> CAS_Def.T list |