equal
deleted
inserted
replaced
56 (* ind_cases method *) |
56 (* ind_cases method *) |
57 |
57 |
58 val setup = |
58 val setup = |
59 Method.setup @{binding "ind_cases"} |
59 Method.setup @{binding "ind_cases"} |
60 (Scan.lift (Scan.repeat1 Args.name_source) >> |
60 (Scan.lift (Scan.repeat1 Args.name_source) >> |
61 (fn props => fn ctxt => Method.erule 0 (map (smart_cases ctxt) props))) |
61 (fn props => fn ctxt => Method.erule ctxt 0 (map (smart_cases ctxt) props))) |
62 "dynamic case analysis on sets"; |
62 "dynamic case analysis on sets"; |
63 |
63 |
64 |
64 |
65 (* outer syntax *) |
65 (* outer syntax *) |
66 |
66 |