| changeset 41296 | 6aaf80ea9715 |
| parent 40832 | 4352ca878c41 |
| child 42083 | e1209fc7ecdc |
| 41295:5b5388d4ccc9 | 41296:6aaf80ea9715 |
|---|---|
10 val cont_tac: int -> tactic |
10 val cont_tac: int -> tactic |
11 val cont_proc: theory -> simproc |
11 val cont_proc: theory -> simproc |
12 val setup: theory -> theory |
12 val setup: theory -> theory |
13 end |
13 end |
14 |
14 |
15 structure ContProc :> CONT_PROC = |
15 structure ContProc : CONT_PROC = |
16 struct |
16 struct |
17 |
17 |
18 (** theory context references **) |
18 (** theory context references **) |
19 |
19 |
20 val cont_K = @{thm cont_const} |
20 val cont_K = @{thm cont_const} |