Mercurial Mercurial > wneuper > isa / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Interpret/ctree-access.sml
changeset 59298 4a57be56d601
parent 59294 f1f2f113f965
child 59299 bf6e43b9ce92 
     1.1 --- a/src/Tools/isac/Interpret/ctree-access.sml	Thu Jan 19 11:35:30 2017 +0100
     1.2 +++ b/src/Tools/isac/Interpret/ctree-access.sml	Sat Jan 21 10:25:19 2017 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4    val cappend_form :  CTbasic.ctree ->  CTbasic.pos ->  CTbasic.istate * Proof.context -> term ->
     1.5      CTbasic.ctree *  CTbasic.pos' list
     1.6    val cappend_problem : CTbasic.ctree -> CTbasic.pos -> CTbasic.istate * Proof.context ->
     1.7 -    CTbasic.fmz -> ori list * spec * term -> CTbasic.ctree * CTbasic.pos' list
     1.8 +    Selem.fmz -> ori list * spec * term -> CTbasic.ctree * CTbasic.pos' list
     1.9    val append_result : CTbasic.ctree -> CTbasic.pos -> CTbasic.istate * Proof.context ->
    1.10      CTbasic.result -> CTbasic.ostate -> CTbasic.ctree * 'a list
    1.11    val append_atomic :                                                          (* for solve.sml *)
    1.12 @@ -34,12 +34,12 @@
    1.13  (* ---- for tests only: made visible in order to remove the warning --------------------------- *)
    1.14    val cappend_parent : CTbasic.ctree -> int list -> CTbasic.istate * Proof.context -> term ->
    1.15      CTbasic.tac -> CTbasic.branch -> CTbasic.ctree * CTbasic.pos' list
    1.16 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.17 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    1.18    val update_loc' : CTbasic.ctree -> CTbasic.pos ->
    1.19      (CTbasic.istate * Proof.context) option * (CTbasic.istate * Proof.context) option -> CTbasic.ctree
    1.20 -  val append_problem : int list -> CTbasic.istate * Proof.context -> CTbasic.fmz ->
    1.21 +  val append_problem : int list -> CTbasic.istate * Proof.context -> Selem.fmz ->
    1.22      ori list * spec * term -> CTbasic.ctree -> CTbasic.ctree
    1.23 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.24 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.25  end
    1.26  (**)
    1.27  structure CTaccess(**): CALC_TREE_ACCESS(**) =
wneuper/isa