equal
deleted
inserted
replaced
31 loopers: string list, |
31 loopers: string list, |
32 unsafe_solvers: string list, |
32 unsafe_solvers: string list, |
33 safe_solvers: string list} |
33 safe_solvers: string list} |
34 type simproc |
34 type simproc |
35 val eq_simproc: simproc * simproc -> bool |
35 val eq_simproc: simproc * simproc -> bool |
36 val morph_simproc: morphism -> simproc -> simproc |
36 val transform_simproc: morphism -> simproc -> simproc |
37 val make_simproc: {name: string, lhss: cterm list, |
37 val make_simproc: {name: string, lhss: cterm list, |
38 proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc |
38 proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc |
39 val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc |
39 val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc |
40 val addsimps: simpset * thm list -> simpset |
40 val addsimps: simpset * thm list -> simpset |
41 val delsimps: simpset * thm list -> simpset |
41 val delsimps: simpset * thm list -> simpset |
623 proc: morphism -> simpset -> cterm -> thm option, |
623 proc: morphism -> simpset -> cterm -> thm option, |
624 id: stamp * thm list}; |
624 id: stamp * thm list}; |
625 |
625 |
626 fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2); |
626 fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2); |
627 |
627 |
628 fun morph_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) = |
628 fun transform_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) = |
629 Simproc |
629 Simproc |
630 {name = name, |
630 {name = name, |
631 lhss = map (Morphism.cterm phi) lhss, |
631 lhss = map (Morphism.cterm phi) lhss, |
632 proc = Morphism.transform phi proc, |
632 proc = Morphism.transform phi proc, |
633 id = (s, Morphism.fact phi ths)}; |
633 id = (s, Morphism.fact phi ths)}; |