(*

 structure Ctree :

 sig

   val Ets : ets exception PTREE of string

   val append_atomic :

      pos -> istate * Proof.context -> term -> tac -> term * term list -> ostate -> ctree -> ctree

   val append_form : int list -> istate * Proof.context -> term -> ctree -> ctree

   val append_parent : pos -> istate * Proof.context -> term -> tac -> branch -> ctree -> ctree

   val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree -> ctree

   val append_result : ctree -> pos -> istate * Proof.context -> term * term list -> ostate -> ctree * 'a list

   val appl_branch : (ppobj -> bool) * (posel -> ctree list -> ctree list) -> ctree -> int list -> ctree * bool

   val appl_obj : (ppobj -> ppobj) -> ctree -> pos -> ctree

   val appl_to_node : (ppobj -> ppobj) -> ctree -> ctree

   datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB

   val branch2str : branch -> string

   val cappend_atomic :

      ctree -> pos -> istate * Proof.context -> term -> tac -> term * term list -> ostate -> ctree * pos' list

   val cappend_form : ctree -> pos -> istate * Proof.context -> term -> ctree * pos' list

   val cappend_parent : ctree -> pos -> istate * Proof.context -> term -> tac -> branch -> ctree * pos' list

   val cappend_problem :

      ctree -> int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree * pos' list

   eqtype cellID

   val children : ctree -> ctree list

   type cid = cellID list

   datatype con = land | lor

   val cut_bottom : pos * posel -> ctree -> (ctree * pos' list) * bool

   val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list

   val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list

   val cut_levup : pos' list -> bool -> ctree -> ctree -> posel list * posel -> ctree -> ctree * pos' list

   val cut_tree : ctree -> pos * 'a -> ctree * pos' list

   val cutlevup : ppobj -> bool

   val del_res : ppobj -> ppobj

   val delete_result : ctree -> pos -> ctree

   val e_ctxt : Proof.context

   val e_fmz : 'a list * spec

   val e_ocalhd : bool * pos_ * term * itm list * (bool * term) list * spec

   val e_origin : ori list * spec * term

   val e_ptform : ptform

   val e_ptform' : ptform

   val e_ctree : ctree

   val e_scrstate : scrstate

   val e_sube : cterm' list

   val e_subs : string list

   val e_subte : term list

   val empty_envp : envp type env = (term * term) list

   type envp = (int * term list) list * (int * rls) list * (int * ets) list * (string * pos) list

   val eq_tac : tac * tac -> bool type ets = (loc_ * (tac_ * env * env * term * term * safe)) list

   val ets2s : loc_ * (tac_ * subst * subst * term * term * safe) -> string

   val ets2str : ets -> string

   val exist_lev_on' : ctree -> pos' -> bool

   val existpt : pos -> ctree -> bool

   val existpt' : pos' -> ctree -> bool

   type fmz = fmz_ * spec

   type fmz_ = cterm' list

   val g_branch : ppobj -> branch

   val g_cell : ppobj -> lrd option

   val g_ctxt : ppobj -> Proof.context

   val g_domID : ppobj -> domID

   val g_env : ppobj -> (istate * Proof.context) option

   val g_fmz : ppobj -> fmz

   val g_form : ppobj -> term

   val g_form' : ctree -> term

   val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option

   val g_met : ppobj -> itm list

   val g_metID : ppobj -> metID

   val g_origin : ppobj -> ori list * spec * term

   val g_ostate : ppobj -> ostate

   val g_ostate' : ctree -> ostate

   val g_pbl : ppobj -> itm list

   val g_res : ppobj -> term

   val g_res' : ctree -> term

   val g_result : ppobj -> term * term list

   val g_spec : ppobj -> spec

   val g_tac : ppobj -> tac

   val get_all : (ppobj -> 'a) -> ctree -> 'a list

   val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list

   val get_allpos' : pos * posel -> ctree -> pos' list

   val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list

   val get_allps : (pos * pos_) list -> posel list -> ctree list -> pos' list

   val get_alls : (ppobj -> 'a) -> ctree list -> 'a list

   val get_assumptions_ : ctree -> pos * pos_ -> term list

   val get_ctxt : ctree -> pos * pos_ -> Proof.context

   val get_curr_formula : ctree * (pos * pos_) -> term

   val get_istate : ctree -> pos * pos_ -> istate

   val get_loc : ctree -> pos * pos_ -> istate * Proof.context

   val get_nd : ctree -> pos -> ctree

   val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a

   val get_somespec : spec -> spec -> spec

   val get_somespec' : spec -> spec -> spec

   val get_trace : ctree -> int list -> int list -> int list list

   val gpt_cell : ctree -> lrd option

   type iist = istate option * istate option

   val ind : pos' -> int

   val ins_chn : ctree list -> ctree -> int list -> ctree

   val ins_nth : int -> 'a -> 'a list -> 'a list

   val insert_pt : ppobj -> ctree -> int list -> ctree

   val is_curr_endof_calc : ctree -> pos' -> bool

   val is_e_ctxt : Proof.context -> bool

   val is_empty_tac : tac -> bool

   val is_interpos : pos' -> bool

   val is_pblnd : ctree -> bool

   val is_pblobj : ppobj -> bool

   val is_pblobj' : ctree -> pos -> bool

   val is_prfobj : ppobj -> bool

   val is_rewset : tac -> bool

   val is_rewtac : tac -> bool

   val isasub2subst : term -> (term * term) list

   datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate

   val istate2str : istate -> string

   val istates2str : istate option * istate option -> string

   val just_created : ctree * pos' -> bool

   val just_created_ : ppobj -> bool

   val last_onlev : ctree -> pos -> bool

   val lev_back' : pos' -> pos'

   val lev_dn : posel list -> posel list

   val lev_dnRes : pos' -> pos'

   val lev_dn_ : pos' -> pos'

   val lev_of : pos' -> int

   val lev_on : pos -> posel list

   val lev_on' : ctree -> pos' -> pos'

   val lev_onFrm : pos' -> pos'

   val lev_pred : pos -> pos

   val lev_pred' : ctree -> pos' -> pos'

   val lev_up : pos -> pos

   val lev_up_ : pos' -> pos'

   val move_dn : pos -> ctree -> int list * pos_ -> int list * pos_

   val move_up : int list -> ctree -> int list * pos_ -> int list * pos_

   val movecalchd_up : ctree -> pos' -> pos'

   val movelevel_dn : int list -> ctree -> int list * pos_ -> int list * pos_

   val movelevel_up : int list -> ctree -> int list * pos_ -> int list * pos_

   val new_val : term -> istate -> istate

   val nth : int -> 'a list -> 'a

   type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec

   val ocalhd2str : ocalhd -> string

   datatype ostate = Complete | Incomplete | Inconsistent

   val ostate2str : ostate -> string

   val par_children : ctree -> pos -> ctree list * pos

   val par_pbl_det : ctree -> pos -> bool * pos * rls

   val par_pblobj : ctree -> pos -> pos

   type pos = posel list

   type pos' = pos * pos_

   val pos's2str : (int list * pos_) list -> string

   val pos2str : int list -> string

   datatype pos_ = Frm | Met | Pbl | Res | Und

   val pos_2str : pos_ -> string

   val pos_plus : int -> pos * pos_ -> pos'

   eqtype posel

   val posless : int list -> int list -> bool

   datatype ppobj

   = PblObj of

     {branch: branch,

      cell: lrd option,

      ctxt: Proof.context,

      env: (istate * Proof.context) option,

      fmz: fmz,

      loc: (istate * Proof.context) option * (istate * Proof.context) option,

      meth: itm list,

      origin: ori list * spec * term, ostate: ostate, probl: itm list, result: term * term list, spec: spec}

      | PrfObj of

      {branch: branch,

       cell: lrd option,

       form: term,

       loc: (istate * Proof.context) option * (istate * Proof.context) option,

       ostate: ostate, result: term * term list, tac: tac}

   val pr_pos : int list -> string

   val pr_ctree : (pos -> ppobj -> string) -> ctree -> string

   val pr_short : pos -> ppobj -> string

   val pre_pos : pos -> pos

   val preconds2str : (bool * term) list -> string

   datatype ptform = Form of term | ModSpec of ocalhd

   datatype ctree = EmptyPtree | Nd of ppobj * ctree list

   val rep_pblobj :

      ppobj ->

      {branch: branch,

       cell: lrd option,

       ctxt: Proof.context,

       env: (istate * Proof.context) option,

       fmz: fmz,

       loc: (istate * Proof.context) option * (istate * Proof.context) option,

       meth: itm list,

       origin: ori list * spec * term, ostate: ostate, probl: itm list, result: term * term list, spec: spec}

   val rep_prfobj :

      ppobj ->

      {branch: branch,

       cell: lrd option,

       form: term,

       loc: (istate * Proof.context) option * (istate * Proof.context) option,

       ostate: ostate, result: term * term list, tac: tac}

   val repl : 'a list -> int -> 'a -> 'a list

   val repl_app : 'a list -> int -> 'a -> 'a list

   val repl_branch : branch -> ppobj -> ppobj

   val repl_ctxt : Proof.context -> ppobj -> ppobj

   val repl_domID : domID -> ppobj -> ppobj

   val repl_env : (istate * Proof.context) option -> ppobj -> ppobj

   val repl_form : term -> ppobj -> ppobj

   val repl_loc : (istate * Proof.context) option * (istate * Proof.context) option -> ppobj -> ppobj

   val repl_met : itm list -> ppobj -> ppobj

   val repl_metID : metID -> ppobj -> ppobj

   val repl_oris : ori list -> ppobj -> ppobj

   val repl_orispec : spec -> ppobj -> ppobj

   val repl_pbl : itm list -> ppobj -> ppobj

   val repl_pblID : pblID -> ppobj -> ppobj

   val repl_result :

      (istate * Proof.context) option * (istate * Proof.context) option ->

      term * term list -> ostate -> ppobj -> ppobj

   val repl_spec : spec -> ppobj -> ppobj

   val repl_tac : tac -> ppobj -> ppobj

   val res2str : term * term list -> string

   val rls_of : tac -> rls'

   val rls_of_rewset : tac -> rls' * subst option

   val rootthy : ctree -> theory

   val rta2str : rule * (term * term list) -> string

   val rule2tac : theory -> (term * term) list -> rule -> tac

   val safe2str : safe -> string

   type scrstate = env * loc_ * term option * term * safe * bool

   val scrstate2str : subst * loc_ * term option * term * safe * bool -> string

   val str2pos_ : string -> pos_

   type sube = cterm' list

   val sube2str : string list -> string

   val sube2subst : theory -> string list -> (term * term) list

   val sube2subte : string list -> term list

   type subs = cterm' list

   val subs2subst : theory -> string list -> (term * term) list

   val subst2sube : (term * term) list -> string list

   val subst2subs : (term * term) list -> string list

   val subst2subs' : (term * term) list -> (string * string) list

   type subte = term list

   val subte2str : term list -> string

   val subte2sube : term list -> string list

   val subte2subst : term list -> (term * term) list

   datatype tac

   = Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm' | Apply_Assumption of cterm' list

      | Apply_Method of metID | Begin_Sequ | Begin_Trans | CAScmd of cterm' | Calculate of string

      | Check_Postcond of pblID | Check_elementwise of cterm' | Collect_Trues | Conclude_And | Conclude_Or

      | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm' | Derive of rls' | Detail_Set of rls'

      | Detail_Set_Inst of subs * rls' | Empty_Tac | End_Detail | End_Intersect | End_Proof' | End_Ruleset

      | End_Sequ | End_Subproblem | End_Trans | Free_Solve | Group of con * int list

      | Init_Proof of cterm' list * spec | Model_Problem | Or_to_List | Refine_Problem of pblID

      | Refine_Tacitly of pblID | Rewrite of thm'' | Rewrite_Asm of thm'' | Rewrite_Inst of subs * thm''

      | Rewrite_Set of rls' | Rewrite_Set_Inst of subs * rls' | Specify_Method of metID

      | Specify_Problem of pblID | Specify_Theory of domID | Split_And | Split_Intersect | Split_Or

      | Subproblem of domID * pblID | Substitute of sube | Tac of string | Take of cterm' | Take_Inst of cterm'

   val tac2IDstr : tac -> string

   datatype tac_

   = Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list

      | Apply_Assumption' of term list * term | Apply_Method' of metID * term option * istate * Proof.context

      | Begin_Sequ' | Begin_Trans' of term | CAScmd' of term

      | Calculate' of theory' * string * term * (term * thm') | Check_Postcond' of pblID * (term * term list)

      | Check_elementwise' of term * string * (term * term list) | Collect_Trues' of term

      | Conclude_And' of term | Conclude_Or' of term | Del_Find' of cterm' | Del_Given' of cterm'

      | Del_Relation' of cterm' | Derive' of rls

      | Detail_Set' of theory' * bool * rls * term * (term * term list)

      | Detail_Set_Inst' of theory' * bool * subst * rls * term * (term * term list) | Empty_Tac_

      | End_Detail' of term * term list | End_Intersect' of term | End_Proof'' | End_Ruleset' of term

      | End_Sequ' | End_Subproblem' of term | End_Trans' of term * term list | Free_Solve'

      | Group' of con * int list * term | Init_Proof' of cterm' list * spec

      | Model_Problem' of pblID * itm list * itm list | Or_to_List' of term * term

      | Refine_Problem' of pblID * (itm list * (bool * term) list)

      | Refine_Tacitly' of pblID * pblID * domID * metID * itm list

      | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * (term * term list)

      | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * (term * term list)

      | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * (term * term list)

      | Rewrite_Set' of theory' * bool * rls * term * (term * term list)

      | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * (term * term list)

      | Specify_Method' of metID * ori list * itm list

      | Specify_Problem' of pblID * (bool * (itm list * (bool * term) list)) | Specify_Theory' of domID

      | Split_And' of term | Split_Intersect' of term | Split_Or' of term

      | Subproblem' of spec * ori list * term * fmz_ * Proof.context * term

      | Substitute' of rew_ord_ * rls * subte * term * term | Tac_ of theory * string * string * string

      | Take' of term | Take_Inst' of term

   val tac_2str : tac_ -> string

   val test_trans : ppobj -> bool

   val thm_of_rew : tac -> thmID * subst option

   val topt2str : term option -> string

   val update_branch : ctree -> pos -> branch -> ctree

   val update_ctxt : ctree -> pos -> Proof.context -> ctree

   val update_domID : ctree -> pos -> domID -> ctree

   val update_env : ctree -> pos -> (istate * Proof.context) option -> ctree

   val update_loc' : ctree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ctree

   val update_met : ctree -> pos -> itm list -> ctree

   val update_metID : ctree -> pos -> metID -> ctree

   val update_metppc : ctree -> pos -> itm list -> ctree

   val update_oris : ctree -> pos -> ori list -> ctree

   val update_orispec : ctree -> pos -> spec -> ctree

   val update_pbl : ctree -> pos -> itm list -> ctree

   val update_pblID : ctree -> pos -> pblID -> ctree

   val update_pblppc : ctree -> pos -> itm list -> ctree

   val update_spec : ctree -> pos -> spec -> ctree

   val update_tac : ctree -> pos -> tac -> ctree end

 *)