| author | Walther Neuper <walther.neuper@jku.at> |
| Wed, 29 Apr 2020 12:30:51 +0200 | |
| changeset 59920 | 33913fe24685 |
| child 59921 | 0766dade4a78 |
| permissions | -rw-r--r-- |
| walther@59920 | 1 |
(* Title: Specify/solve-step.sml |
| walther@59920 | 2 |
Author: Walther Neuper |
| walther@59920 | 3 |
(c) due to copyright terms |
| walther@59920 | 4 |
|
| walther@59920 | 5 |
Code for the solve-phase in analogy to structure Specify_Step for the specify-phase. |
| walther@59920 | 6 |
*) |
| walther@59920 | 7 |
|
| walther@59920 | 8 |
signature SOLVE_STEP = |
| walther@59920 | 9 |
sig |
| walther@59920 | 10 |
val check_appl: Pos.pos' -> CTbasic.ctree -> Tactic.input -> Applicable.T |
| walther@59920 | 11 |
end |
| walther@59920 | 12 |
|
| walther@59920 | 13 |
(**) |
| walther@59920 | 14 |
structure Solve_Step(** ): SOLVE_STEP( **) = |
| walther@59920 | 15 |
struct |
| walther@59920 | 16 |
(**) |
| walther@59920 | 17 |
|
| walther@59920 | 18 |
(*-----^^^^^- specify -----vvvvv- solve --------------------------------------------------------*) |
| walther@59920 | 19 |
(*-----^^^^^- solve ---------------------------------------------------------------------------*) |
| walther@59920 | 20 |
|
| walther@59920 | 21 |
|
| walther@59920 | 22 |
|
| walther@59920 | 23 |
(**)end(**); |