1.1 --- a/src/Tools/isac/CalcElements/rule.sml	Mon Apr 06 11:44:36 2020 +0200
     1.2 +++ b/src/Tools/isac/CalcElements/rule.sml	Wed Apr 08 12:32:51 2020 +0200
     1.3 @@ -15,42 +15,46 @@
     1.4    datatype rule = datatype Rule_Def.rule
     1.5    datatype program = datatype Rule_Def.program
     1.6  
     1.7 +(*/------- to exec-def.sml ------------------------\*)
     1.8    eqtype calID
     1.9    type eval_fn = Rule_Def.eval_fn
    1.10 +(*\------- to exec-def.sml ------------------------/*)
    1.11  
    1.12    eqtype cterm'
    1.13    type subst = (term * term) list
    1.14  
    1.15 +(*/------- to rewrite-ord.sml ---------------------\*)
    1.16    val dummy_ord: Rule_Def.rew_ord_
    1.17    val e_rew_ord_: Rule_Def.rew_ord_
    1.18    val e_rew_ord: Rule_Def.rew_ord_
    1.19    val e_rew_ordX: Rule_Def.rew_ord
    1.20    val rew_ord': (Rule_Def.rew_ord' * (subst -> term * term -> bool)) list Unsynchronized.ref
    1.21    val assoc_rew_ord: string -> subst -> term * term -> bool
    1.22 +(*\------- to rewrite-ord.sml ---------------------/*)
    1.23  
    1.24    eqtype errpatID                                                              (*..from Rule_Def*)
    1.25    type errpat = errpatID * term list * thm list
    1.26  
    1.27    val scr2str: program -> string
    1.28  
    1.29 -  val thy2ctxt: theory -> Proof.context                      (* shift up in sequence of defs *)
    1.30 -  val thy2ctxt': string -> Proof.context                     (* shift up in sequence of defs *)
    1.31 -  val Thy_Info_get_theory: string -> theory                  (* shift up in sequence of defs *)
    1.32 +(*/------- to theoryC.sml -------------------------\*)
    1.33 +  val thy2ctxt: theory -> Proof.context
    1.34 +  val thy2ctxt': string -> Proof.context
    1.35 +  val Thy_Info_get_theory: string -> theory
    1.36 +  eqtype thyID
    1.37 +  eqtype domID
    1.38 +  val e_domID: domID
    1.39 +  eqtype theory'
    1.40 +  val theory'2thyID: theory' -> theory'
    1.41 +  val theory2theory': theory -> theory'
    1.42 +  val theory2thyID: theory -> thyID
    1.43 +  val thyID2theory': thyID -> thyID
    1.44 +  val string_of_thy: theory -> theory'
    1.45 +  val theory2domID: theory -> theory'
    1.46 +  val Isac: 'a -> theory
    1.47 +  val string_of_thmI: thm -> string
    1.48 +(*\------- to theoryC.sml -------------------------/*)
    1.49  
    1.50 -  eqtype thyID                                               (* shift up in sequence of defs *)
    1.51 -  eqtype domID                                               (* shift up in sequence of defs *)
    1.52 -  val e_domID: domID                                         (* shift up in sequence of defs *)
    1.53 -  eqtype theory'                                             (* shift up in sequence of defs *)
    1.54 -  val theory'2thyID: theory' -> theory'                      (* shift up in sequence of defs *)
    1.55 -  val theory2theory': theory -> theory'                      (* shift up in sequence of defs *)
    1.56 -  val theory2thyID: theory -> thyID                          (* shift up in sequence of defs *)
    1.57 -  val thyID2theory': thyID -> thyID                          (* shift up in sequence of defs *)
    1.58 -  val string_of_thy: theory -> theory'                       (* shift up in sequence of defs *)
    1.59 -  val theory2domID: theory -> theory'                        (* shift up in sequence of defs *)
    1.60 -
    1.61 -  val Isac: 'a -> theory                                     (* shift up in sequence of defs *)
    1.62 -
    1.63 -  val string_of_thmI: thm -> string                          (* shift up to Unparse *)
    1.64    val e_term: term                                           (* shift up to Unparse *)
    1.65    val e_type: typ                                            (* shift up to Unparse *)
    1.66    val type2str: typ -> string