equal
deleted
inserted
replaced
61 |
61 |
62 (* ind_cases method *) |
62 (* ind_cases method *) |
63 |
63 |
64 fun mk_cases_meth (ctxt, props) = |
64 fun mk_cases_meth (ctxt, props) = |
65 props |
65 props |
66 |> map (smart_cases (ProofContext.theory_of ctxt) (Simplifier.get_local_simpset ctxt) |
66 |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) |
67 (ProofContext.read_prop ctxt)) |
67 (ProofContext.read_prop ctxt)) |
68 |> Method.erule 0; |
68 |> Method.erule 0; |
69 |
69 |
70 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name)); |
70 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name)); |
71 |
71 |