equal
deleted
inserted
replaced
32 val rule = |
32 val rule = |
33 (case opt_rule of |
33 (case opt_rule of |
34 SOME rule => rule |
34 SOME rule => rule |
35 | NONE => |
35 | NONE => |
36 (case Induct.find_casesT ctxt |
36 (case Induct.find_casesT ctxt |
37 (#2 (check_type ctxt (ProofContext.read_term_schematic ctxt s))) of |
37 (#2 (check_type ctxt (Proof_Context.read_term_schematic ctxt s))) of |
38 rule :: _ => rule |
38 rule :: _ => rule |
39 | [] => @{thm case_split})); |
39 | [] => @{thm case_split})); |
40 val _ = Method.trace ctxt [rule]; |
40 val _ = Method.trace ctxt [rule]; |
41 |
41 |
42 val xi = |
42 val xi = |