Lines Matching refs:solver
803 datatype solver = Solver of simpls -> thm list -> term -> thm;
813 fun Rewrite Once (Simpls(ss,thl),Context cntxt,Congs congs,Solver solver) =
814 RW_STEPS ONCE_DEPTH (ss,cntxt,congs,solver) thl
816 | Rewrite Fully (Simpls(ss,thl),Context cntxt,Congs congs,Solver solver) =
817 RW_STEPS TOP_DEPTH (ss,cntxt,congs,solver) thl
819 | Rewrite(Special f)(Simpls(ss,thl),Context cntxt,Congs congs,Solver solver) =
820 RW_STEPS f (ss,cntxt,congs,solver) thl
822 | Rewrite Once (Default thl,Context cntxt,Congs congs,Solver solver) =
824 cntxt,congs,solver) thl
826 | Rewrite Once (Pure thl,Context cntxt,Congs congs,Solver solver) =
827 RW_STEPS ONCE_DEPTH (empty_simpls,cntxt,congs,solver) thl
829 | Rewrite Fully (Default thl,Context cntxt,Congs congs,Solver solver) =
831 cntxt,congs,solver) thl
833 | Rewrite Fully (Pure thl,Context cntxt,Congs congs,Solver solver) =
834 RW_STEPS TOP_DEPTH (empty_simpls,cntxt,congs,solver) thl
836 | Rewrite (Special f) (Default thl,Context cntxt,Congs congs,Solver solver) =
837 RW_STEPS f (implicit_simpls(),cntxt,congs,solver) thl
839 | Rewrite (Special f) (Pure thl,Context cntxt,Congs congs,Solver solver) =
840 RW_STEPS f (empty_simpls,cntxt,congs,solver) thl;
880 fun solver_err() = raise RW_ERR "solver error" "";