equal
deleted
inserted
replaced
52 SS{mss=mss, |
52 SS{mss=mss, |
53 simps= simps, |
53 simps= simps, |
54 congs= congs, |
54 congs= congs, |
55 subgoal_tac= subgoal_tac, |
55 subgoal_tac= subgoal_tac, |
56 finish_tac=finish_tac, |
56 finish_tac=finish_tac, |
57 loop_tac=loop_tac}; |
57 loop_tac= DETERM o loop_tac}; |
58 |
58 |
59 fun (SS{mss,simps,congs,subgoal_tac,loop_tac,...}) setsolver finish_tac = |
59 fun (SS{mss,simps,congs,subgoal_tac,loop_tac,...}) setsolver finish_tac = |
60 SS{mss=mss, |
60 SS{mss=mss, |
61 simps= simps, |
61 simps= simps, |
62 congs= congs, |
62 congs= congs, |