equal
deleted
inserted
replaced
48 type method |
48 type method |
49 val method: (thm list -> tactic) -> method |
49 val method: (thm list -> tactic) -> method |
50 val method_cases: (thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq) -> method |
50 val method_cases: (thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq) -> method |
51 val refine: (context -> method) -> state -> state Seq.seq |
51 val refine: (context -> method) -> state -> state Seq.seq |
52 val refine_end: (context -> method) -> state -> state Seq.seq |
52 val refine_end: (context -> method) -> state -> state Seq.seq |
53 val export_thm: context -> thm -> thm |
|
54 val match_bind: (string list * string) list -> state -> state |
53 val match_bind: (string list * string) list -> state -> state |
55 val match_bind_i: (term list * term) list -> state -> state |
54 val match_bind_i: (term list * term) list -> state -> state |
56 val let_bind: (string list * string) list -> state -> state |
55 val let_bind: (string list * string) list -> state -> state |
57 val let_bind_i: (term list * term) list -> state -> state |
56 val let_bind_i: (term list * term) list -> state -> state |
58 val simple_have_thms: string -> thm list -> state -> state |
57 val simple_have_thms: string -> thm list -> state -> state |
428 val _ = print_rule rule; |
427 val _ = print_rule rule; |
429 val thmq = FINDGOAL (refine_tac rule) thm; |
428 val thmq = FINDGOAL (refine_tac rule) thm; |
430 in Seq.map (fn th => map_goal I (K ((result, (facts, th)), f)) state) thmq end; |
429 in Seq.map (fn th => map_goal I (K ((result, (facts, th)), f)) state) thmq end; |
431 in raw_rule |> exp_tac |> (Seq.flat o Seq.map exp_rule) end; |
430 in raw_rule |> exp_tac |> (Seq.flat o Seq.map exp_rule) end; |
432 |
431 |
433 fun export_thm inner thm = |
|
434 let val exp_tac = ProofContext.export_wrt false inner None in |
|
435 (case Seq.chop (2, exp_tac thm) of |
|
436 ([thm'], _) => thm' |
|
437 | ([], _) => raise THM ("export: failed", 0, [thm]) |
|
438 | _ => raise THM ("export: more than one result", 0, [thm])) |
|
439 end; |
|
440 |
|
441 fun transfer_facts inner_state state = |
432 fun transfer_facts inner_state state = |
442 (case get_facts inner_state of |
433 (case get_facts inner_state of |
443 None => Seq.single (reset_facts state) |
434 None => Seq.single (reset_facts state) |
444 | Some thms => |
435 | Some thms => |
445 let |
436 let |