src/Provers/simplifier.ML
changeset 433 1e4f420523ae
parent 406 4d4e0442b106
child 983 6f80fed73e29
equal deleted inserted replaced
432:0d1071ac599c 433:1e4f420523ae
    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,