equal
deleted
inserted
replaced
47 (Args.T list -> modifier * Args.T list) list -> |
47 (Args.T list -> modifier * Args.T list) list -> |
48 (thm list -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method |
48 (thm list -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method |
49 val only_sectioned_args: |
49 val only_sectioned_args: |
50 (Args.T list -> modifier * Args.T list) list -> |
50 (Args.T list -> modifier * Args.T list) list -> |
51 (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method |
51 (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method |
|
52 val thms_ctxt_args: (thm list -> Proof.context -> Proof.method) |
|
53 -> Args.src -> Proof.context -> Proof.method |
52 val thms_args: (thm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method |
54 val thms_args: (thm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method |
53 datatype text = |
55 datatype text = |
54 Basic of (Proof.context -> Proof.method) | |
56 Basic of (Proof.context -> Proof.method) | |
55 Source of Args.src | |
57 Source of Args.src | |
56 Then of text list | |
58 Then of text list | |
295 in f x ctxt' end; |
297 in f x ctxt' end; |
296 |
298 |
297 fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f; |
299 fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f; |
298 fun only_sectioned_args ss f = sectioned_args (Scan.succeed ()) ss (fn () => f); |
300 fun only_sectioned_args ss f = sectioned_args (Scan.succeed ()) ss (fn () => f); |
299 |
301 |
300 fun thms_args f = sectioned_args (thmss []) [] (fn ths => fn _ => f ths); |
302 fun thms_ctxt_args f = sectioned_args (thmss []) [] f; |
|
303 fun thms_args f = thms_ctxt_args (K o f); |
301 |
304 |
302 end; |
305 end; |
303 |
306 |
304 |
307 |
305 |
308 |