equal
deleted
inserted
replaced
46 -> ProofHistory.T -> ProofHistory.T |
46 -> ProofHistory.T -> ProofHistory.T |
47 val using_facts: (string * Args.src list) list list -> ProofHistory.T -> ProofHistory.T |
47 val using_facts: (string * Args.src list) list list -> ProofHistory.T -> ProofHistory.T |
48 val using_facts_i: (thm * Proof.context attribute list) list list |
48 val using_facts_i: (thm * Proof.context attribute list) list list |
49 -> ProofHistory.T -> ProofHistory.T |
49 -> ProofHistory.T -> ProofHistory.T |
50 val chain: ProofHistory.T -> ProofHistory.T |
50 val chain: ProofHistory.T -> ProofHistory.T |
|
51 val instantiate_locale: string * string -> ProofHistory.T -> ProofHistory.T |
51 val fix: (string list * string option) list -> ProofHistory.T -> ProofHistory.T |
52 val fix: (string list * string option) list -> ProofHistory.T -> ProofHistory.T |
52 val fix_i: (string list * typ option) list -> ProofHistory.T -> ProofHistory.T |
53 val fix_i: (string list * typ option) list -> ProofHistory.T -> ProofHistory.T |
53 val let_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T |
54 val let_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T |
54 val let_bind_i: (term list * term) list -> ProofHistory.T -> ProofHistory.T |
55 val let_bind_i: (term list * term) list -> ProofHistory.T -> ProofHistory.T |
55 val invoke_case: string * string option list * Args.src list -> ProofHistory.T -> ProofHistory.T |
56 val invoke_case: string * string option list * Args.src list -> ProofHistory.T -> ProofHistory.T |
288 |
289 |
289 val using_facts_i = ProofHistory.apply o Proof.using_thmss_i o map (map (apfst single)); |
290 val using_facts_i = ProofHistory.apply o Proof.using_thmss_i o map (map (apfst single)); |
290 |
291 |
291 val chain = ProofHistory.apply Proof.chain; |
292 val chain = ProofHistory.apply Proof.chain; |
292 |
293 |
|
294 (* locale instantiation *) |
|
295 |
|
296 fun instantiate_locale (prfx, loc) = |
|
297 ProofHistory.apply (Proof.instantiate_locale (loc, prfx)); |
293 |
298 |
294 (* context *) |
299 (* context *) |
295 |
300 |
296 val fix = ProofHistory.apply o Proof.fix; |
301 val fix = ProofHistory.apply o Proof.fix; |
297 val fix_i = ProofHistory.apply o Proof.fix_i; |
302 val fix_i = ProofHistory.apply o Proof.fix_i; |