73 

    73 

    74 ML {*

    74 ML {*

    75 fun strip_prems_concl trm =

    75 fun strip_prems_concl trm =

    76   (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm)

    76   (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm)

    77 *}

    77 *}

    79 

    78 

    80 ML {*

    79 ML {*

    81   @{thms foo.exhaust}

    80   @{thms foo.exhaust}

    82   |> map prop_of

    81   |> map prop_of

    83   |> map strip_prems_concl

    82   |> map strip_prems_concl